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

proof

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;

hence meet {X,Y} = X /\ Y by XBOOLE_0:def 4; :: thesis: verum