take 0 ; :: thesis: 0 is zero
thus 0 = 0 ; :: according to ORDINAL1:def 14 :: thesis: verum