let D be set ; :: thesis: for F being Subset-Family of D st F <> {} holds
([#] D) \ () = meet ()

let F be Subset-Family of D; :: thesis: ( F <> {} implies ([#] D) \ () = meet () )
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 ;
then not x in Y ` by A3;
hence x in Y by ; :: 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 ;
then x in X ` by A5;
hence not x in X by XBOOLE_0:def 5; :: thesis: verum
end;
assume F <> {} ; :: thesis: ([#] D) \ () = meet ()
then A7: COMPLEMENT F <> {} by Th32;
A8: ([#] D) \ () c= meet ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ([#] D) \ () or x in meet () )
assume A9: x in ([#] D) \ () ; :: thesis: x in meet ()
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 () by ; :: thesis: verum
end;
meet () c= ([#] D) \ ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet () or x in ([#] D) \ () )
assume A10: x in meet () ; :: thesis: x in ([#] D) \ ()
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) \ () by ; :: thesis: verum
end;
hence ([#] D) \ () = meet () by A8; :: thesis: verum