now :: thesis: for x being object holds
( x in {2} /\ {3} iff contradiction )
let x be object ; :: thesis: ( x in {2} /\ {3} iff contradiction )
( x in {2} /\ {3} iff ( x in {2} & x in {3} ) ) by XBOOLE_0:def 4;
then ( x in {2} /\ {3} iff ( x = 2 & x = 3 ) ) by TARSKI:def 1;
hence ( x in {2} /\ {3} iff contradiction ) ; :: thesis: verum
end;
hence {2} /\ {3} = {} by XBOOLE_0:def 1; :: thesis: verum