let X, SFY be set ; :: thesis: ( SFY <> {} implies X \ (union SFY) = meet (DIFFERENCE ({X},SFY)) )

set y = the Element of SFY;

A1: X in {X} by TARSKI:def 1;

assume SFY <> {} ; :: thesis: X \ (union SFY) = meet (DIFFERENCE ({X},SFY))

then A2: X \ the Element of SFY in DIFFERENCE ({X},SFY) by A1, Def6;

A3: meet (DIFFERENCE ({X},SFY)) c= X \ (union SFY)

set y = the Element of SFY;

A1: X in {X} by TARSKI:def 1;

assume SFY <> {} ; :: thesis: X \ (union SFY) = meet (DIFFERENCE ({X},SFY))

then A2: X \ the Element of SFY in DIFFERENCE ({X},SFY) by A1, Def6;

A3: meet (DIFFERENCE ({X},SFY)) c= X \ (union SFY)

proof

X \ (union SFY) c= meet (DIFFERENCE ({X},SFY))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (DIFFERENCE ({X},SFY)) or x in X \ (union SFY) )

assume A4: x in meet (DIFFERENCE ({X},SFY)) ; :: thesis: x in X \ (union SFY)

for Z being set st Z in SFY holds

not x in Z

not Z in SFY ;

then A5: not x in union SFY by TARSKI:def 4;

x in X \ the Element of SFY by A2, A4, Def1;

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

end;assume A4: x in meet (DIFFERENCE ({X},SFY)) ; :: thesis: x in X \ (union SFY)

for Z being set st Z in SFY holds

not x in Z

proof

then
for Z being set st x in Z holds
let Z be set ; :: thesis: ( Z in SFY implies not x in Z )

assume Z in SFY ; :: thesis: not x in Z

then X \ Z in DIFFERENCE ({X},SFY) by A1, Def6;

then x in X \ Z by A4, Def1;

hence not x in Z by XBOOLE_0:def 5; :: thesis: verum

end;assume Z in SFY ; :: thesis: not x in Z

then X \ Z in DIFFERENCE ({X},SFY) by A1, Def6;

then x in X \ Z by A4, Def1;

hence not x in Z by XBOOLE_0:def 5; :: thesis: verum

not Z in SFY ;

then A5: not x in union SFY by TARSKI:def 4;

x in X \ the Element of SFY by A2, A4, Def1;

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

proof

hence
X \ (union SFY) = meet (DIFFERENCE ({X},SFY))
by A3; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (union SFY) or x in meet (DIFFERENCE ({X},SFY)) )

assume x in X \ (union SFY) ; :: thesis: x in meet (DIFFERENCE ({X},SFY))

then A6: ( x in X & not x in union SFY ) by XBOOLE_0:def 5;

for Z being set st Z in DIFFERENCE ({X},SFY) holds

x in Z

end;assume x in X \ (union SFY) ; :: thesis: x in meet (DIFFERENCE ({X},SFY))

then A6: ( x in X & not x in union SFY ) by XBOOLE_0:def 5;

for Z being set st Z in DIFFERENCE ({X},SFY) holds

x in Z

proof

hence
x in meet (DIFFERENCE ({X},SFY))
by A2, Def1; :: thesis: verum
let Z be set ; :: thesis: ( Z in DIFFERENCE ({X},SFY) implies x in Z )

assume Z in DIFFERENCE ({X},SFY) ; :: thesis: x in Z

then consider Z1, Z2 being set such that

A7: ( Z1 in {X} & Z2 in SFY ) and

A8: Z = Z1 \ Z2 by Def6;

( x in Z1 & not x in Z2 ) by A6, A7, TARSKI:def 1, TARSKI:def 4;

hence x in Z by A8, XBOOLE_0:def 5; :: thesis: verum

end;assume Z in DIFFERENCE ({X},SFY) ; :: thesis: x in Z

then consider Z1, Z2 being set such that

A7: ( Z1 in {X} & Z2 in SFY ) and

A8: Z = Z1 \ Z2 by Def6;

( x in Z1 & not x in Z2 ) by A6, A7, TARSKI:def 1, TARSKI:def 4;

hence x in Z by A8, XBOOLE_0:def 5; :: thesis: verum