let X be set ; :: thesis: for S being non empty Subset-Family of X holds
( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
let S be non empty Subset-Family of X; :: thesis: ( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
thus meet S = X \ (union (X \ S)) :: thesis: union S = X \ (meet (X \ S))

proof

thus meet S c= X \ (union (X \ S)) :: according to XBOOLE_0:def 10 :: thesis: X \ (union (X \ S)) c= meet S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet S or x in X \ (union (X \ S)) )
assume A1: x in meet S ; :: thesis: x in X \ (union (X \ S))
not x in union (X \ S)

proof

assume x in union (X \ S) ; :: thesis: contradiction
then consider Z being set such that
A2: ( x in Z & Z in X \ S ) by TARSKI:def 4;
reconsider Z = Z as Subset of X by A2;
A3: Z ` in S by A2, SETFAM_1:def 8;
not x in Z ` by A2, XBOOLE_0:def 5;
hence contradiction by A1, A3, SETFAM_1:def 1; :: thesis: verum

end;

hence x in X \ (union (X \ S)) by A1, XBOOLE_0:def 5; :: thesis: verum

end;

thus X \ (union (X \ S)) c= meet S :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (union (X \ S)) or x in meet S )
assume A4: x in X \ (union (X \ S)) ; :: thesis: x in meet S
then A5: ( x in X & not x in union (X \ S) ) by XBOOLE_0:def 5;
for Y being set st Y in S holds
x in Y

proof

let Y be set ; :: thesis: ( Y in S implies x in Y )
assume that
A6: Y in S and
A7: not x in Y ; :: thesis: contradiction
reconsider Y = Y as Subset of X by A6;
A8: x in Y ` by A4, A7, SUBSET_1:50;
(Y ` ) ` in S by A6;
then Y ` in X \ S by SETFAM_1:def 8;
hence contradiction by A5, A8, TARSKI:def 4; :: thesis: verum

end;

hence x in meet S by SETFAM_1:def 1; :: thesis: verum

end;

end;

thus union S c= X \ (meet (X \ S)) :: according to XBOOLE_0:def 10 :: thesis: X \ (meet (X \ S)) c= union S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union S or x in X \ (meet (X \ S)) )
assume x in union S ; :: thesis: x in X \ (meet (X \ S))
then consider Y being set such that
A9: ( x in Y & Y in S ) by TARSKI:def 4;
reconsider Y = Y as Subset of X by A9;
not x in meet (X \ S)

proof

assume A10: x in meet (X \ S) ; :: thesis: contradiction
(Y ` ) ` in S by A9;
then A11: Y ` in X \ S by SETFAM_1:def 8;
not x in Y ` by A9, XBOOLE_0:def 5;
hence contradiction by A10, A11, SETFAM_1:def 1; :: thesis: verum

end;

hence x in X \ (meet (X \ S)) by A9, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (meet (X \ S)) or x in union S )
assume A12: x in X \ (meet (X \ S)) ; :: thesis: x in union S
then ( x in X & not x in meet (X \ S) ) by XBOOLE_0:def 5;
then consider Z being set such that
A13: ( Z in X \ S & not x in Z ) by SETFAM_1:def 1;
reconsider Z = Z as Subset of X by A13;
ex Y being set st
( Y in S & x in Y )

proof

A14: Z ` in S by A13, SETFAM_1:def 8;
x in Z ` by A12, A13, SUBSET_1:50;
hence ex Y being set st
( Y in S & x in Y ) by A14; :: thesis: verum

end;

hence x in union S by TARSKI:def 4; :: thesis: verum