let X, SFY be set ; :: thesis: ( SFY <> {} implies X \ (union SFY) = meet (DIFFERENCE {X},SFY) )
assume A1: SFY <> {} ; :: thesis: X \ (union SFY) = meet (DIFFERENCE {X},SFY)
consider y being Element of SFY;
A2: X in {X} by TARSKI:def 1;
then A3: X \ y in DIFFERENCE {X},SFY by A1, Def6;
A4: 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 A5: ( 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
A6: ( Z1 in {X} & Z2 in SFY & Z = Z1 \ Z2 ) by Def6;
( x in Z1 & not x in Z2 ) by A5, A6, TARSKI:def 1, TARSKI:def 4;
hence x in Z by A6, XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

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 A7: x in meet (DIFFERENCE {X},SFY) ; :: thesis: x in X \ (union SFY)
then A8: x in X \ y by A3, Def1;
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 A2, Def6;
then x in X \ Z by A7, 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 not x in union SFY by TARSKI:def 4;
hence x in X \ (union SFY) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

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