take {0} ; :: thesis: not {0} is zero
thus {0} <> 0 ; :: according to ORDINAL1:def 14 :: thesis: verum