let x, Z, y be set ; :: thesis: ( x in Z & y in Z implies {x,y} /\ Z = {x,y} )
assume ( x in Z & y in Z ) ; :: thesis: {x,y} /\ Z = {x,y}
then {x,y} c= Z by Th38;
hence {x,y} /\ Z = {x,y} by XBOOLE_1:28; :: thesis: verum