let a, b be positive ExtInt; :: thesis: ( a in X & ( for i being positive ExtInt st i in X holds
a <= i ) & b in X & ( for i being positive ExtInt st i in X holds
b <= i ) implies a = b )
assume ( a in X & ( for i being positive ExtInt st i in X holds
a <= i ) & b in X & ( for i being positive ExtInt st i in X holds
b <= i ) ) ; :: thesis: a = b
then ( a <= b & b <= a ) ;
hence a = b by XXREAL_0:1; :: thesis: verum