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

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

suppose t in NAT ; :: thesis: t <= t

hence t <= t by Def33; :: thesis: verum

end;

suppose A2: not t in NAT ; :: thesis: t <= t

then t in (QC-symbols A) \ NAT by XBOOLE_0:def 5;
then [t,t] in the Relation of A by A1, RELAT_2:def 1;
hence t <= t by A2, Def33; :: thesis: verum

end;

end;