take 0 ; :: thesis: 0 is ordinal-membered
take 0 ; :: according to ORDINAL6:def 1 :: thesis: 0 c= 0
thus 0 c= 0 ; :: thesis: verum