let x, y be set ; :: thesis: {x} /\ {x,y} = {x}
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence {x} /\ {x,y} = {x} by Lm9; :: thesis: verum