let A be QC-alphabet ; :: thesis: for t, u being QC-symbol of A holds
( t <= u or u <= t )
let t, u be QC-symbol of A; :: thesis: ( t <= u or u <= t )
set R = the Relation of A;
the Relation of A well_orders (QC-symbols A) \ NAT by Def32;
then ( the Relation of A is_connected_in (QC-symbols A) \ NAT & the Relation of A is_reflexive_in (QC-symbols A) \ NAT ) by WELLORD1:def 5;
then A1: the Relation of A is_strongly_connected_in (QC-symbols A) \ NAT by ORDERS_1:7;

per cases ( ( t in NAT & u in NAT ) or not t in NAT or not u in NAT ) ;

suppose A2: ( t in NAT & u in NAT ) ; :: thesis: ( t <= u or u <= t )

then consider n, m being Nat such that
A3: ( n = t & m = u ) ;
( n <= m or m <= n ) ;
hence ( t <= u or u <= t ) by A3, Def33, A2; :: thesis: verum

end;

suppose ( not t in NAT or not u in NAT ) ; :: thesis: ( t <= u or u <= t )

per cases then ( not t in NAT or not u in NAT ) ;

suppose A4: not t in NAT ; :: thesis: ( t <= u or u <= t )

per cases ( u in NAT or not u in NAT ) ;

suppose u in NAT ; :: thesis: ( t <= u or u <= t )

hence ( t <= u or u <= t ) by A4, Def33; :: thesis: verum

end;

suppose A5: not u in NAT ; :: thesis: ( t <= u or u <= t )

then ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A4, XBOOLE_0:def 5;
then ( [t,u] in the Relation of A or [u,t] in the Relation of A ) by A1, RELAT_2:def 7;
hence ( t <= u or u <= t ) by A4, A5, Def33; :: thesis: verum

end;

end;

end;

suppose A6: not u in NAT ; :: thesis: ( t <= u or u <= t )

per cases ( t in NAT or not t in NAT ) ;

suppose t in NAT ; :: thesis: ( t <= u or u <= t )

hence ( t <= u or u <= t ) by A6, Def33; :: thesis: verum

end;

suppose A7: not t in NAT ; :: thesis: ( t <= u or u <= t )

then ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A6, XBOOLE_0:def 5;
then ( [u,t] in the Relation of A or [t,u] in the Relation of A ) by A1, RELAT_2:def 7;
hence ( t <= u or u <= t ) by A6, A7, Def33; :: thesis: verum

end;

end;

end;

end;

end;

end;