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

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

end;

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

hence meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY) ; :: thesis: verum

end;

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

then
meet (DIFFERENCE (SFX,SFY)) = {}
by Def1;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 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

hence meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY) ; :: thesis: verum

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

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;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

then A5:
x in meet SFX
by A3, Def1;
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;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

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