let x, y be Element of 1; :: thesis: ( op2 . (x,y) = 0 iff x = y )
A1: ( x = {} & y = {} ) by CARD_1:49, TARSKI:def 1;
hence ( op2 . (x,y) = 0 implies x = y ) ; :: thesis: ( x = y implies op2 . (x,y) = 0 )
thus ( x = y implies op2 . (x,y) = 0 ) by A1, Lm2; :: thesis: verum