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

A1: X \ (union (X \ S)) c= meet S

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

assume A14: x in X \ (meet (X \ S)) ; :: thesis: x in union S

then not x in meet (X \ S) by XBOOLE_0:def 5;

then consider Z being set such that

A15: Z in X \ S and

A16: not x in Z by SETFAM_1:def 1;

reconsider Z = Z as Subset of X by A15;

A17: Z ` in S by A15, SETFAM_1:def 7;

x in Z ` by A14, A16, SUBSET_1:29;

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

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

A1: X \ (union (X \ S)) c= meet S

proof

meet S c= X \ (union (X \ S))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (union (X \ S)) or x in meet S )

assume A2: x in X \ (union (X \ S)) ; :: thesis: x in meet S

then A3: not x in union (X \ S) by XBOOLE_0:def 5;

for Y being set st Y in S holds

x in Y

end;assume A2: x in X \ (union (X \ S)) ; :: thesis: x in meet S

then A3: not x in union (X \ S) by XBOOLE_0:def 5;

for Y being set st Y in S holds

x in Y

proof

hence
x in meet S
by SETFAM_1:def 1; :: thesis: verum
let Y be set ; :: thesis: ( Y in S implies x in Y )

assume that

A4: Y in S and

A5: not x in Y ; :: thesis: contradiction

reconsider Y = Y as Subset of X by A4;

(Y `) ` in S by A4;

then A6: Y ` in X \ S by SETFAM_1:def 7;

x in Y ` by A2, A5, SUBSET_1:29;

hence contradiction by A3, A6, TARSKI:def 4; :: thesis: verum

end;assume that

A4: Y in S and

A5: not x in Y ; :: thesis: contradiction

reconsider Y = Y as Subset of X by A4;

(Y `) ` in S by A4;

then A6: Y ` in X \ S by SETFAM_1:def 7;

x in Y ` by A2, A5, SUBSET_1:29;

hence contradiction by A3, A6, TARSKI:def 4; :: thesis: verum

proof

hence
meet S = X \ (union (X \ S))
by A1; :: thesis: union S = X \ (meet (X \ S))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet S or x in X \ (union (X \ S)) )

assume A7: x in meet S ; :: thesis: x in X \ (union (X \ S))

not x in union (X \ S)

end;assume A7: x in meet S ; :: thesis: x in X \ (union (X \ S))

not x in union (X \ S)

proof

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

then consider Z being set such that

A8: x in Z and

A9: Z in X \ S by TARSKI:def 4;

reconsider Z = Z as Subset of X by A9;

( Z ` in S & not x in Z ` ) by A8, A9, SETFAM_1:def 7, XBOOLE_0:def 5;

hence contradiction by A7, SETFAM_1:def 1; :: thesis: verum

end;then consider Z being set such that

A8: x in Z and

A9: Z in X \ S by TARSKI:def 4;

reconsider Z = Z as Subset of X by A9;

( Z ` in S & not x in Z ` ) by A8, A9, SETFAM_1:def 7, XBOOLE_0:def 5;

hence contradiction by A7, SETFAM_1:def 1; :: thesis: verum

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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (meet (X \ S)) or x in union S )
let x be object ; :: 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

A10: x in Y and

A11: Y in S by TARSKI:def 4;

reconsider Y = Y as Subset of X by A11;

not x in meet (X \ S)

end;assume x in union S ; :: thesis: x in X \ (meet (X \ S))

then consider Y being set such that

A10: x in Y and

A11: Y in S by TARSKI:def 4;

reconsider Y = Y as Subset of X by A11;

not x in meet (X \ S)

proof

hence
x in X \ (meet (X \ S))
by A10, A11, XBOOLE_0:def 5; :: thesis: verum
(Y `) ` in S
by A11;

then A12: Y ` in X \ S by SETFAM_1:def 7;

assume A13: x in meet (X \ S) ; :: thesis: contradiction

not x in Y ` by A10, XBOOLE_0:def 5;

hence contradiction by A13, A12, SETFAM_1:def 1; :: thesis: verum

end;then A12: Y ` in X \ S by SETFAM_1:def 7;

assume A13: x in meet (X \ S) ; :: thesis: contradiction

not x in Y ` by A10, XBOOLE_0:def 5;

hence contradiction by A13, A12, SETFAM_1:def 1; :: thesis: verum

assume A14: x in X \ (meet (X \ S)) ; :: thesis: x in union S

then not x in meet (X \ S) by XBOOLE_0:def 5;

then consider Z being set such that

A15: Z in X \ S and

A16: not x in Z by SETFAM_1:def 1;

reconsider Z = Z as Subset of X by A15;

A17: Z ` in S by A15, SETFAM_1:def 7;

x in Z ` by A14, A16, SUBSET_1:29;

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