let R be Relation; :: thesis: ( R is well-ordering implies ( R is being_quasi-order & R is being_partial-order & R is being_linear-order ) )
assume ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) ; :: according to WELLORD1:def 4 :: thesis: ( R is being_quasi-order & R is being_partial-order & R is being_linear-order )
hence ( R is reflexive & R is transitive & R is reflexive & R is transitive & R is antisymmetric & R is reflexive & R is transitive & R is antisymmetric & R is connected ) ; :: according to ORDERS_1:def 3,ORDERS_1:def 4,ORDERS_1:def 5 :: thesis: verum