let p1, p2 be positive Pell's_solution of D; :: thesis: ( ( for p being positive Pell's_solution of D holds
( p1 `1 <= p `1 & p1 `2 <= p `2 ) ) & ( for p being positive Pell's_solution of D holds
( p2 `1 <= p `1 & p2 `2 <= p `2 ) ) implies p1 = p2 )
assume that
A5: for p being positive Pell's_solution of D holds
( p1 `1 <= p `1 & p1 `2 <= p `2 ) and
A6: for p being positive Pell's_solution of D holds
( p2 `1 <= p `1 & p2 `2 <= p `2 ) ; :: thesis: p1 = p2
( p1 `1 <= p2 `1 & p1 `1 >= p2 `1 & p1 `2 <= p2 `2 & p1 `2 >= p2 `2 ) by A5, A6;
then A7: ( p1 `1 = p2 `1 & p1 `2 = p2 `2 ) by XXREAL_0:1;
( p1 = [(p1 `1),(p1 `2)] & p2 = [(p2 `1),(p2 `2)] ) ;
hence p1 = p2 by A7; :: thesis: verum