let X1, X2 be Subset-Family of (bool Omega); :: thesis: ( ( for S being Subset-Family of Omega holds
( S in X1 iff ex E being finite Subset of I st S = sigUn F,(I \ E) ) ) & ( for S being Subset-Family of Omega holds
( S in X2 iff ex E being finite Subset of I st S = sigUn F,(I \ E) ) ) implies X1 = X2 )
assume A1: for S being Subset-Family of Omega holds
( S in X1 iff ex E being finite Subset of I st S = sigUn F,(I \ E) ) ; :: thesis: ( ex S being Subset-Family of Omega st
( ( S in X2 implies ex E being finite Subset of I st S = sigUn F,(I \ E) ) implies ( ex E being finite Subset of I st S = sigUn F,(I \ E) & not S in X2 ) ) or X1 = X2 )
assume A2: for S being Subset-Family of Omega holds
( S in X2 iff ex E being finite Subset of I st S = sigUn F,(I \ E) ) ; :: thesis: X1 = X2

now

let S be Subset-Family of Omega; :: thesis: ( S in X1 iff S in X2 )
( ( S in X1 implies ex E being finite Subset of I st S = sigUn F,(I \ E) ) & ( ex E being finite Subset of I st S = sigUn F,(I \ E) implies S in X1 ) & ( S in X2 implies ex E being finite Subset of I st S = sigUn F,(I \ E) ) & ( ex E being finite Subset of I st S = sigUn F,(I \ E) implies S in X2 ) ) by A1, A2;
hence ( S in X1 iff S in X2 ) ; :: thesis: verum

end;

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