let x, y be ExtReal; :: thesis: ( x less_pred y or y less_pred x or x = y )
assume ( not x less_pred y & not y less_pred x ) ; :: thesis: x = y
then ( x <= y & x >= y ) ;
hence x = y by XXREAL_0:1; :: thesis: verum