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

( 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 )

hence
X1 = X2
by SUBSET_1:3; :: thesis: verum( 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;( 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