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

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

meet (UNION ({X},SFY)) c= X \/ (meet SFY)
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

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

hence
x in meet (UNION ({X},SFY))
by A2, Def1; :: thesis: verum
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;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

proof

hence
X \/ (meet SFY) = meet (UNION ({X},SFY))
by A3; :: thesis: verum
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;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