let D be set ; :: thesis:
let F be Subset-Family of D; :: thesis:
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:
assume A2: x in D ; :: thesis:
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:

proof

assume A3: for X being set st X in F holds
not x in X ; :: thesis:
let Y be set ; :: thesis:
assume A4: Y in COMPLEMENT F ; :: thesis:
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:

end;

assume A5: for Y being set st Y in COMPLEMENT F holds
x in Y ; :: thesis:
let X be set ; :: thesis:
assume A6: X in F ; :: thesis:
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:

end;

assume F <> {} ; :: thesis:
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:
assume A9: x in ([#] D) \ (union F) ; :: thesis:
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:

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in meet (COMPLEMENT F) ; :: thesis:
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:

end;

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