let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in REAL or not y in REAL or x = y or [x,y] in RealOrd or [y,x] in RealOrd )
assume ( x in REAL & y in REAL ) ; :: thesis: ( x = y or [x,y] in RealOrd or [y,x] in RealOrd )
then reconsider x = x, y = y as Element of REAL ;
( x <= y or y <= x ) ;
hence ( x = y or [x,y] in RealOrd or [y,x] in RealOrd ) ; :: thesis: verum