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 ( t in NAT & u in NAT ) ; :: thesis: ( t <= u or u <= t )

then consider n, m being Element of NAT such that
A2: ( n = t & m = u ) ;
( n <= m or m <= n ) ;
hence ( t <= u or u <= t ) by A2, Def33; :: 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 A3: 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 A3, Def33; :: thesis: verum

end;

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

then ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A3, 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 A3, A4, Def33; :: thesis: verum

end;

end;

end;

suppose A5: 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 A5, Def33; :: thesis: verum

end;

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

then ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A5, 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 A5, A6, Def33; :: thesis: verum

end;

end;

end;

end;

end;

end;