let A be QC-alphabet ; :: thesis: for s, t being QC-symbol of A holds
( s < t iff not t <= s )
let s, t be QC-symbol of A; :: thesis: ( s < t iff not t <= s )
thus ( s < t implies not t <= s ) :: thesis: ( not t <= s implies s < t )

proof

assume s < t ; :: thesis: not t <= s
then A1: ( s <= t & not s = t ) by Def34;
assume t <= s ; :: thesis: contradiction
hence contradiction by A1, Th23; :: thesis: verum

end;

assume not t <= s ; :: thesis: s < t
then ( s <= t & not t = s ) by Th24;
hence s < t by Def34; :: thesis: verum