let X, SFY be set ; :: thesis: ( SFY <> {} implies X \ (meet SFY) = union (DIFFERENCE {X},SFY) )
assume A1: SFY <> {} ; :: thesis: X \ (meet SFY) = union (DIFFERENCE {X},SFY)
A2: X in {X} by TARSKI:def 1;
A3: X \ (meet SFY) c= union (DIFFERENCE {X},SFY)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (meet SFY) or x in union (DIFFERENCE {X},SFY) )
assume A4: x in X \ (meet SFY) ; :: thesis: x in union (DIFFERENCE {X},SFY)
then ( x in X & not x in meet SFY ) by XBOOLE_0:def 5;
then consider Z being set such that
A5: ( Z in SFY & not x in Z ) by A1, Def1;
A6: X \ Z in DIFFERENCE {X},SFY by A2, A5, Def6;
x in X \ Z by A4, A5, XBOOLE_0:def 5;
hence x in union (DIFFERENCE {X},SFY) by A6, TARSKI:def 4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (DIFFERENCE {X},SFY) or x in X \ (meet SFY) )
assume x in union (DIFFERENCE {X},SFY) ; :: thesis: x in X \ (meet SFY)
then consider Z being set such that
A7: ( x in Z & Z in DIFFERENCE {X},SFY ) by TARSKI:def 4;
consider Z1, Z2 being set such that
A8: ( Z1 in {X} & Z2 in SFY & Z = Z1 \ Z2 ) by A7, Def6;
A9: Z1 = X by A8, TARSKI:def 1;
then ( x in X & not x in Z2 ) by A7, A8, XBOOLE_0:def 5;
then not x in meet SFY by A8, Def1;
hence x in X \ (meet SFY) by A7, A8, A9, XBOOLE_0:def 5; :: thesis: verum

end;

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