let D be set ; :: thesis: for F being Subset-Family of D st F <> {} holds
([#] D) \ (union F) = meet (COMPLEMENT F)
let F be Subset-Family of D; :: thesis: ( F <> {} implies ([#] D) \ (union F) = meet (COMPLEMENT F) )
A1: for x being object st x in D holds
( ( for X being set st X in F holds
not x in X ) iff for Y being set st Y in COMPLEMENT F holds
x in Y )

proof

let x be object ; :: thesis: ( x in D implies ( ( for X being set st X in F holds
not x in X ) iff for Y being set st Y in COMPLEMENT F holds
x in Y ) )
assume A2: x in D ; :: thesis: ( ( for X being set st X in F holds
not x in X ) iff for Y being set st Y in COMPLEMENT F holds
x in Y )
thus ( ( for X being set st X in F holds
not x in X ) implies for Y being set st Y in COMPLEMENT F holds
x in Y ) :: thesis: ( ( for Y being set st Y in COMPLEMENT F holds
x in Y ) implies for X being set st X in F holds
not x in X )

proof

assume A3: for X being set st X in F holds
not x in X ; :: thesis: for Y being set st Y in COMPLEMENT F holds
x in Y
let Y be set ; :: thesis: ( Y in COMPLEMENT F implies x in Y )
assume A4: Y in COMPLEMENT F ; :: thesis: x in Y
then reconsider Y = Y as Subset of D ;
Y ` in F by A4, Def7;
then not x in Y ` by A3;
hence x in Y by A2, XBOOLE_0:def 5; :: thesis: verum

end;

assume A5: for Y being set st Y in COMPLEMENT F holds
x in Y ; :: thesis: for X being set st X in F holds
not x in X
let X be set ; :: thesis: ( X in F implies not x in X )
assume A6: X in F ; :: thesis: not x in X
then reconsider X = X as Subset of D ;
(X `) ` = X ;
then X ` in COMPLEMENT F by A6, Def7;
then x in X ` by A5;
hence not x in X by XBOOLE_0:def 5; :: thesis: verum

end;

assume F <> {} ; :: thesis: ([#] D) \ (union F) = meet (COMPLEMENT F)
then A7: COMPLEMENT F <> {} by Th32;
A8: ([#] D) \ (union F) c= meet (COMPLEMENT F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ([#] D) \ (union F) or x in meet (COMPLEMENT F) )
assume A9: x in ([#] D) \ (union F) ; :: thesis: x in meet (COMPLEMENT F)
then not x in union F by XBOOLE_0:def 5;
then for X being set st X in F holds
not x in X by TARSKI:def 4;
then for Y being set st Y in COMPLEMENT F holds
x in Y by A1, A9;
hence x in meet (COMPLEMENT F) by A7, Def1; :: thesis: verum

end;

meet (COMPLEMENT F) c= ([#] D) \ (union F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (COMPLEMENT F) or x in ([#] D) \ (union F) )
assume A10: x in meet (COMPLEMENT F) ; :: thesis: x in ([#] D) \ (union F)
then for X being set st X in COMPLEMENT F holds
x in X by Def1;
then for Y being set st x in Y holds
not Y in F by A1;
then not x in union F by TARSKI:def 4;
hence x in ([#] D) \ (union F) by A10, XBOOLE_0:def 5; :: thesis: verum

end;

hence ([#] D) \ (union F) = meet (COMPLEMENT F) by A8; :: thesis: verum