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

now :: thesis: for S being Subset of Omega holds
( 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;

hence X1 = X2 by SUBSET_1:3; :: thesis: verum