let X, SFY be set ; :: thesis: ( SFY <> {} implies X \/ (meet SFY) = meet (UNION ({X},SFY)) )
assume A1: SFY <> {} ; :: thesis: X \/ (meet SFY) = meet (UNION ({X},SFY))
set y = the Element of SFY;
X in {X} by TARSKI:def 1;
then A2: X \/ the Element of SFY in UNION ({X},SFY) by A1, Def4;
A3: X \/ (meet SFY) c= meet (UNION ({X},SFY))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \/ (meet SFY) or x in meet (UNION ({X},SFY)) )
assume x in X \/ (meet SFY) ; :: thesis: x in meet (UNION ({X},SFY))
then A4: ( x in X or x in meet SFY ) by XBOOLE_0:def 3;
for Z being set st Z in UNION ({X},SFY) holds
x in Z
proof
let Z be set ; :: thesis: ( Z in UNION ({X},SFY) implies x in Z )
assume Z in UNION ({X},SFY) ; :: thesis: x in Z
then consider Z1, Z2 being set such that
A5: ( Z1 in {X} & Z2 in SFY ) and
A6: Z = Z1 \/ Z2 by Def4;
( x in Z1 or x in Z2 ) by A4, A5, Def1, TARSKI:def 1;
hence x in Z by A6, XBOOLE_0:def 3; :: thesis: verum
end;
hence x in meet (UNION ({X},SFY)) by A2, Def1; :: thesis: verum
end;
meet (UNION ({X},SFY)) c= X \/ (meet SFY)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (UNION ({X},SFY)) or x in X \/ (meet SFY) )
assume A7: x in meet (UNION ({X},SFY)) ; :: thesis: x in X \/ (meet SFY)
assume A8: not x in X \/ (meet SFY) ; :: thesis: contradiction
then A9: not x in X by XBOOLE_0:def 3;
not x in meet SFY by A8, XBOOLE_0:def 3;
then consider Z being set such that
A10: Z in SFY and
A11: not x in Z by A1, Def1;
X in {X} by TARSKI:def 1;
then X \/ Z in UNION ({X},SFY) by A10, Def4;
then x in X \/ Z by A7, Def1;
hence contradiction by A9, A11, XBOOLE_0:def 3; :: thesis: verum
end;
hence X \/ (meet SFY) = meet (UNION ({X},SFY)) by A3; :: thesis: verum