for A being Ordinal holds
( ( A <> 0 & A <> 1 ) iff not A is trivial )