let s, t be QC-symbol of A; :: thesis: ( ( for t being QC-symbol of A holds s <= t ) & ( for t being QC-symbol of A holds t <= t ) implies s = t )
assume A1: ( ( for u being QC-symbol of A holds s <= u ) & ( for u being QC-symbol of A holds t <= u ) ) ; :: thesis: s = t
( s <= t & t <= s ) by A1;
hence s = t by Th23; :: thesis: verum