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