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)

proof

let x be set ; :: 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

proof

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;

then for Z being set st x in Z holds
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;

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

proof

let x be set ; :: 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

proof

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;

hence x in meet (DIFFERENCE ({X},SFY)) by A2, Def1; :: thesis: verum

end;

hence X \ (union SFY) = meet (DIFFERENCE ({X},SFY)) by A3, XBOOLE_0:def 10; :: thesis: verum