let A be Ordinal; ( ( A <> 0 & A <> 1 ) iff not A is trivial )
hereby ( not A is trivial implies ( A <> 0 & A <> 1 ) )
end;
assume
not A is trivial
; ( 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 )
; verum