REAL c= dom RealOrd

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL or x in dom RealOrd )
assume A1: x in REAL ; :: thesis: x in dom RealOrd
reconsider x = x as Element of REAL by A1;
[x,x] in RealOrd ;
hence x in dom RealOrd by RELAT_1:def 4; :: thesis: verum

end;

then dom RealOrd = REAL by XBOOLE_0:def 10;
hence RealOrd is total by PARTFUN1:def 4; :: thesis: ( RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is reflexive by Lm1, Th10, RELAT_2:def 9; :: thesis: ( RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is antisymmetric by Lm2, Th10, RELAT_2:def 12; :: thesis: ( RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is transitive by Lm3, Th10, RELAT_2:def 16; :: thesis: RealOrd is being_linear-order
thus RealOrd is_reflexive_in field RealOrd by Lm1, Th10; :: according to RELAT_2:def 9,ORDERS_1:def 5 :: thesis: ( RealOrd is transitive & RealOrd is antisymmetric & RealOrd is connected )
thus RealOrd is_transitive_in field RealOrd by Lm3, Th10; :: according to RELAT_2:def 16 :: thesis: ( RealOrd is antisymmetric & RealOrd is connected )
thus RealOrd is_antisymmetric_in field RealOrd by Lm2, Th10; :: according to RELAT_2:def 12 :: thesis: RealOrd is connected
thus RealOrd is_connected_in field RealOrd by Lm4, Th10; :: according to RELAT_2:def 14 :: thesis: verum