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 :: according to ORDERS_1:def 3 :: thesis: ( R is transitive & R is being_partial-order & R is being_linear-order & R is well-ordering )

proof

let x be set ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field R or [x,x] in R )
assume x in field R ; :: thesis: [x,x] in R
hence [x,x] in R by A1; :: thesis: verum

end;

thus A3: R is transitive :: thesis: ( R is being_partial-order & R is being_linear-order & R is well-ordering )

proof

let x be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for b₁, b₂ being set holds
( not x in field R or not b₁ in field R or not b₂ in field R or not [x,b₁] in R or not [b₁,b₂] in R or [x,b₂] in R )
let y, z be set ; :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume x in field R ; :: thesis: ( not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
thus ( not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) by A1; :: thesis: verum

end;

hence ( R is reflexive & R is transitive ) by A2; :: according to ORDERS_1:def 4 :: thesis: ( R is antisymmetric & R is being_linear-order & R is well-ordering )
thus A4: R is antisymmetric :: thesis: ( R is being_linear-order & R is well-ordering )

proof

let x be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for b₁ being set holds
( not x in field R or not b₁ in field R or not [x,b₁] in R or not [b₁,x] in R or x = b₁ )
let y be set ; :: thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y )
assume x in field R ; :: thesis: ( not y in field R or not [x,y] in R or not [y,x] in R or x = y )
thus ( not y in field R or not [x,y] in R or not [y,x] in R or x = y ) by A1; :: thesis: verum

end;

hence ( R is reflexive & R is transitive & R is antisymmetric ) by A2, A3; :: according to ORDERS_1:def 5 :: thesis: ( R is connected & R is well-ordering )
thus R is connected :: thesis: R is well-ordering

proof

let x be set ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for b₁ being set holds
( not x in field R or not b₁ in field R or x = b₁ or [x,b₁] in R or [b₁,x] in R )
let y be set ; :: thesis: ( not x in field R or not y in field R or x = y or [x,y] in R or [y,x] in R )
assume x in field R ; :: thesis: ( not y in field R or x = y or [x,y] in R or [y,x] in R )
thus ( not y in field R or x = y or [x,y] in R or [y,x] in R ) by A1; :: thesis: verum

end;

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 set st
( b₁ in Y & R -Seg b₁ misses Y ) )
assume that
A5: Y c= field R and
A6: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & R -Seg b₁ misses Y )
thus ex b₁ being set st
( b₁ in Y & R -Seg b₁ misses Y ) by A5, A6, A1; :: thesis: verum