thus RealOrd is_reflexive_in REAL ; :: according to ORDERS_1:def 9 :: thesis: ( RealOrd is_transitive_in REAL & RealOrd is_antisymmetric_in REAL & RealOrd is_connected_in REAL )
thus RealOrd is_transitive_in REAL by Lm3; :: thesis: ( RealOrd is_antisymmetric_in REAL & RealOrd is_connected_in REAL )
thus RealOrd is_antisymmetric_in REAL by Lm2; :: thesis: RealOrd is_connected_in REAL
thus RealOrd is_connected_in REAL by Lm4; :: thesis: verum