let R be Relation; :: thesis: for X being set st R well_orders X holds
( R quasi_orders X & R partially_orders X & R linearly_orders X )
let X be set ; :: thesis: ( R well_orders X implies ( R quasi_orders X & R partially_orders X & R linearly_orders X ) )
assume ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ) ; :: according to WELLORD1:def 5 :: thesis: ( R quasi_orders X & R partially_orders X & R linearly_orders X )
hence ( R is_reflexive_in X & R is_transitive_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) ; :: according to ORDERS_1:def 6,ORDERS_1:def 7,ORDERS_1:def 8 :: thesis: verum