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 A3: 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 A4: 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 :: thesis: for S being Subset-Family of Omega holds
( S in X1 iff S in X2 )

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

end;

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