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