let A be QC-alphabet ; :: thesis: for t, u being QC-symbol of A st t <= u & u <= t holds
u = t
let t, u be QC-symbol of A; :: thesis: ( t <= u & u <= t implies u = 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_antisymmetric_in (QC-symbols A) \ NAT by WELLORD1:def 5;
assume A2: ( t <= u & u <= t ) ; :: thesis: u = t

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

suppose A3: ( t in NAT & u in NAT ) ; :: thesis: u = t

then consider n, m being Nat such that
A4: ( t = n & u = m & n <= m ) by A2, Def33;
consider k, j being Nat such that
A5: ( u = k & t = j & k <= j ) by A2, A3, Def33;
thus u = t by A4, A5, XXREAL_0:1; :: thesis: verum

end;

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

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

suppose not t in NAT ; :: thesis: u = t

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

end;

suppose not u in NAT ; :: thesis: u = t

then A8: ( not t in NAT & not u in NAT ) by A2, Def33;
then A9: ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by XBOOLE_0:def 5;
( [t,u] in the Relation of A & [u,t] in the Relation of A ) by A2, A8, Def33;
hence u = t by A1, A9, RELAT_2:def 4; :: thesis: verum

end;

end;

end;

end;