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