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;