let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in REAL or [x,x] in RealOrd )
assume A1: x in REAL ; :: thesis: [x,x] in RealOrd
reconsider x = x as Element of REAL by A1;
x <= x ;
hence [x,x] in RealOrd ; :: thesis: verum