take {{0}} ; :: thesis: ( {{0}} is without_zero & not {{0}} is empty )
thus not 0 in {{0}} by TARSKI:def 1; :: according to ORDINAL1:def 16 :: thesis: not {{0}} is empty
thus not {{0}} is empty ; :: thesis: verum