let R be Relation; :: thesis: ( R is empty implies ( R is being_quasi-order & R is being_partial-order & R is being_linear-order & R is well-ordering ) )
assume A1: R is empty ; :: thesis: ( R is being_quasi-order & R is being_partial-order & R is being_linear-order & R is well-ordering )
thus A2: R is reflexive by A1; :: according to ORDERS_1:def 4 :: thesis: ( R is transitive & R is being_partial-order & R is being_linear-order & R is well-ordering )
thus A3: R is transitive by A1; :: thesis: ( R is being_partial-order & R is being_linear-order & R is well-ordering )
hence ( R is reflexive & R is transitive ) by A2; :: according to ORDERS_1:def 5 :: thesis: ( R is antisymmetric & R is being_linear-order & R is well-ordering )
thus A4: R is antisymmetric by A1; :: thesis: ( R is being_linear-order & R is well-ordering )
hence ( R is reflexive & R is transitive & R is antisymmetric ) by A2, A3; :: according to ORDERS_1:def 6 :: thesis: ( R is connected & R is well-ordering )
thus R is connected by A1; :: thesis: R is well-ordering
hence ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) by A2, A3, A4; :: according to WELLORD1:def 4 :: thesis: R is well_founded
let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field R or Y = {} or ex b₁ being object st
( b₁ in Y & R -Seg b₁ misses Y ) )
assume that
A5: Y c= field R and
A6: Y <> {} ; :: thesis: ex b₁ being object st
( b₁ in Y & R -Seg b₁ misses Y )
thus ex b₁ being object st
( b₁ in Y & R -Seg b₁ misses Y ) by A5, A6, A1; :: thesis: verum