let X1, X2 be Subset-Family of Omega; :: thesis: ( ( for S being Subset of Omega holds

( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) & ( for S being Subset of Omega holds

( S in X2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) implies X1 = X2 )

assume A2: for S being Subset of Omega holds

( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ; :: thesis: ( ex S being Subset of Omega st

( ( S in X2 implies ex E being finite Subset of I st S in sigUn (F,E) ) implies ( ex E being finite Subset of I st S in sigUn (F,E) & not S in X2 ) ) or X1 = X2 )

assume A3: for S being Subset of Omega holds

( S in X2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ; :: thesis: X1 = X2

( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) & ( for S being Subset of Omega holds

( S in X2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) implies X1 = X2 )

assume A2: for S being Subset of Omega holds

( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ; :: thesis: ( ex S being Subset of Omega st

( ( S in X2 implies ex E being finite Subset of I st S in sigUn (F,E) ) implies ( ex E being finite Subset of I st S in sigUn (F,E) & not S in X2 ) ) or X1 = X2 )

assume A3: for S being Subset of Omega holds

( S in X2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ; :: thesis: X1 = X2

now :: thesis: for S being Subset of Omega holds

( S in X1 iff S in X2 )

hence
X1 = X2
by SUBSET_1:3; :: thesis: verum( S in X1 iff S in X2 )

let S be Subset of Omega; :: thesis: ( S in X1 iff S in X2 )

( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) by A2;

hence ( S in X1 iff S in X2 ) by A3; :: thesis: verum

end;( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) by A2;

hence ( S in X1 iff S in X2 ) by A3; :: thesis: verum