let SFX, SFY be set ; :: thesis: meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)

per cases ( SFX = {} or SFY = {} or ( SFX <> {} & SFY <> {} ) ) ;

suppose A1: ( SFX = {} or SFY = {} ) ; :: thesis: meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)

now :: thesis: not DIFFERENCE (SFX,SFY) <> {}

assume DIFFERENCE (SFX,SFY) <> {} ; :: thesis: contradiction
then consider e being object such that
A2: e in DIFFERENCE (SFX,SFY) by XBOOLE_0:def 1;
ex X, Y being set st
( X in SFX & Y in SFY & e = X \ Y ) by A2, Def6;
hence contradiction by A1; :: thesis: verum

end;

then meet (DIFFERENCE (SFX,SFY)) = {} by Def1;
hence meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY) ; :: thesis: verum

end;

suppose A3: ( SFX <> {} & SFY <> {} ) ; :: thesis: meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)

set z = the Element of SFX;
set y = the Element of SFY;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (DIFFERENCE (SFX,SFY)) or x in (meet SFX) \ (meet SFY) )
assume A4: x in meet (DIFFERENCE (SFX,SFY)) ; :: thesis: x in (meet SFX) \ (meet SFY)
for Z being set st Z in SFX holds
x in Z

proof

let Z be set ; :: thesis: ( Z in SFX implies x in Z )
assume Z in SFX ; :: thesis: x in Z
then Z \ the Element of SFY in DIFFERENCE (SFX,SFY) by A3, Def6;
then x in Z \ the Element of SFY by A4, Def1;
hence x in Z ; :: thesis: verum

end;

then A5: x in meet SFX by A3, Def1;
the Element of SFX \ the Element of SFY in DIFFERENCE (SFX,SFY) by A3, Def6;
then x in the Element of SFX \ the Element of SFY by A4, Def1;
then not x in the Element of SFY by XBOOLE_0:def 5;
then not x in meet SFY by A3, Def1;
hence x in (meet SFX) \ (meet SFY) by A5, XBOOLE_0:def 5; :: thesis: verum

end;

end;