REAL c= dom RealOrd
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL or x in dom RealOrd )
assume x in REAL ; :: thesis: x in dom RealOrd
then reconsider x = x as Element of REAL ;
[x,x] in RealOrd ;
hence x in dom RealOrd by XTUPLE_0:def 12; :: thesis: verum
end;
then dom RealOrd = REAL ;
hence RealOrd is total by PARTFUN1:def 2; :: thesis: ( RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is reflexive by Lm1, Th5; :: thesis: ( RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is antisymmetric by Lm2, Th5; :: thesis: ( RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is transitive by Lm3, Th5; :: thesis: RealOrd is being_linear-order
thus RealOrd is_reflexive_in field RealOrd by Th5; :: according to RELAT_2:def 9,ORDERS_1:def 6 :: thesis: ( RealOrd is transitive & RealOrd is antisymmetric & RealOrd is connected )
thus RealOrd is_transitive_in field RealOrd by Lm3, Th5; :: according to RELAT_2:def 16 :: thesis: ( RealOrd is antisymmetric & RealOrd is connected )
thus RealOrd is_antisymmetric_in field RealOrd by Lm2, Th5; :: according to RELAT_2:def 12 :: thesis: RealOrd is connected
thus RealOrd is_connected_in field RealOrd by Lm4, Th5; :: according to RELAT_2:def 14 :: thesis: verum