let x, y be Element of 1; :: thesis: ( x <> y implies 0 < Empty^2-to-zero . (x,y) )
x = {} by CARD_1:49, TARSKI:def 1;
hence ( x <> y implies 0 < Empty^2-to-zero . (x,y) ) by CARD_1:49, TARSKI:def 1; :: thesis: verum