let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in REAL or not y in REAL or not [x,y] in RealOrd or not [y,x] in RealOrd or x = y )
assume that
A1: ( x in REAL & y in REAL ) and
A2: ( [x,y] in RealOrd & [y,x] in RealOrd ) ; :: thesis: x = y
reconsider x = x, y = y as Element of REAL by A1;
( x <= y & y <= x ) by A2, Th4;
hence x = y by XXREAL_0:1; :: thesis: verum