let A be Ordinal; :: thesis: ( ( A <> 0 & A <> 1 ) iff not A is trivial )

hereby :: thesis: ( not A is trivial implies ( A <> 0 & A <> 1 ) )

assume A1: ( A <> 0 & A <> 1 ) ; :: thesis: not A is trivial
then ( A in 1 or 1 in A ) by ORDINAL1:14;
then A2: 1 in A by A1, CARD_1:49, TARSKI:def 1;
0 in 1 by CARD_1:49, TARSKI:def 1;
then 0 in A by A2, ORDINAL1:10;
hence not A is trivial by A2, ZFMISC_1:def 10; :: thesis: verum

end;

assume not A is trivial ; :: thesis: ( A <> 0 & A <> 1 )
then consider x, y being object such that
A3: ( x in A & y in A & x <> y ) by ZFMISC_1:def 10;
A4: card {x,y} c= card A by A3, ZFMISC_1:32, CARD_1:11;
card A c= A by CARD_1:8;
then card {x,y} c= A by A4, XBOOLE_1:1;
then {0,1} c= A by A3, CARD_2:57, CARD_1:50;
then ( 0 in A & 1 in A ) by ZFMISC_1:32;
hence ( A <> 0 & A <> 1 ) ; :: thesis: verum