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

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