let X, Y be set ; :: thesis: meet {X,Y} = X /\ Y

A1: ( X in {X,Y} & Y in {X,Y} ) by TARSKI:def 2;

for x being object holds

( x in meet {X,Y} iff ( x in X & x in Y ) )

A1: ( X in {X,Y} & Y in {X,Y} ) by TARSKI:def 2;

for x being object holds

( x in meet {X,Y} iff ( x in X & x in Y ) )

proof

hence
meet {X,Y} = X /\ Y
by XBOOLE_0:def 4; :: thesis: verum
let x be object ; :: thesis: ( x in meet {X,Y} iff ( x in X & x in Y ) )

thus ( x in meet {X,Y} implies ( x in X & x in Y ) ) by A1, Def1; :: thesis: ( x in X & x in Y implies x in meet {X,Y} )

assume ( x in X & x in Y ) ; :: thesis: x in meet {X,Y}

then for Z being set st Z in {X,Y} holds

x in Z by TARSKI:def 2;

hence x in meet {X,Y} by Def1; :: thesis: verum

end;thus ( x in meet {X,Y} implies ( x in X & x in Y ) ) by A1, Def1; :: thesis: ( x in X & x in Y implies x in meet {X,Y} )

assume ( x in X & x in Y ) ; :: thesis: x in meet {X,Y}

then for Z being set st Z in {X,Y} holds

x in Z by TARSKI:def 2;

hence x in meet {X,Y} by Def1; :: thesis: verum