Theorem 5.8 (y \in x \in \omega \c y \i x) Note 1 (A \ident \setof x \Each y\in x(y\i x)) By S Note 2 (t \in A \Iff \Each y \in t (y \i t) \And t \in \U) By 08.3;.1 Checked with rules.tex : 84 level: 2 Note 3 (\e \in A) By .2;09.19,09.12 Checked with rules.tex : 148 level: 2 Note 4 (x \in A ) By G Note 5 (x \in \U) By 09.20;.4 Checked with rules.tex : 84 level: 0 Note 6 \Each y \in x(y \i x) By .2;.4 Checked with rules.tex : 116 level: 2 Note 7 Line 1 (y \in \scsr x \c y \in x \Or y = x By 4.7 Checked with rules.tex : 44 level: 0 Line 2 \c y \i x \Or y = x By .6 Checked with rules.tex : 709 level: 0 Line 3 \c y \i x By 011.14 Checked with rules.tex : 663 level: 0 Line 4 \c y \i \scsr x ) By 011.10;( 4.5;(09.20;.4)) Checked with rules.tex : 3033 level: 2 Note 8 (\scsr x \in A) By .2;(4.3;.5),(.7 U) Checked with rules.tex : 3266 level: 2 Note 9 (x \in A \c \scsr x \in A) By .8 H .4 Checked with rules.tex : 2098 level: 0 Note 10 (\omega \i A) By 5.7;.3,(.9 U) Checked with rules.tex : 3124 level: 2 Note 11 Line 1 (y \in x \And x \in \omega\c y \in x \And x \in A By 011.7;.10 Checked with rules.tex : 969 level: 2 Line 2 \c y \in x \And \Each y \in x(y \i x) By .2 Checked with rules.tex : 428 level: 2 Line 3 \c y \i x) By Checked with rules.tex : 2446 level: 2 QED By .11 Checked with rules.tex : 44 level: 2 Proof checked.