thus A1: {} is reflexive :: according to ORDERS_1:def 3 :: thesis: ( {} is transitive & {} is being_partial-order & {} is being_linear-order & {} is well-ordering )

proof

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

end;

thus A2: {} is transitive :: thesis: ( {} is being_partial-order & {} is being_linear-order & {} 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 {} or not b₁ in field {} or not b₂ in field {} or not [x,b₁] in {} or not [b₁,b₂] in {} or [x,b₂] in {} )
let y, z be set ; :: thesis: ( not x in field {} or not y in field {} or not z in field {} or not [x,y] in {} or not [y,z] in {} or [x,z] in {} )
assume x in field {} ; :: thesis: ( not y in field {} or not z in field {} or not [x,y] in {} or not [y,z] in {} or [x,z] in {} )
thus ( not y in field {} or not z in field {} or not [x,y] in {} or not [y,z] in {} or [x,z] in {} ) ; :: thesis: verum

end;

hence ( {} is reflexive & {} is transitive ) by A1; :: according to ORDERS_1:def 4 :: thesis: ( {} is antisymmetric & {} is being_linear-order & {} is well-ordering )
thus A3: {} is antisymmetric :: thesis: ( {} is being_linear-order & {} 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 {} or not b₁ in field {} or not [x,b₁] in {} or not [b₁,x] in {} or x = b₁ )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} or x = y )
assume x in field {} ; :: thesis: ( not y in field {} or not [x,y] in {} or not [y,x] in {} or x = y )
thus ( not y in field {} or not [x,y] in {} or not [y,x] in {} or x = y ) ; :: thesis: verum

end;

hence ( {} is reflexive & {} is transitive & {} is antisymmetric ) by A1, A2; :: according to ORDERS_1:def 5 :: thesis: ( {} is connected & {} is well-ordering )
thus {} is connected :: thesis: {} 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 {} or not b₁ in field {} or x = b₁ or [x,b₁] in {} or [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or x = y or [x,y] in {} or [y,x] in {} )
assume x in field {} ; :: thesis: ( not y in field {} or x = y or [x,y] in {} or [y,x] in {} )
thus ( not y in field {} or x = y or [x,y] in {} or [y,x] in {} ) ; :: thesis: verum

end;

hence ( {} is reflexive & {} is transitive & {} is antisymmetric & {} is connected ) by A1, A2, A3; :: according to WELLORD1:def 4 :: thesis: {} is well_founded
let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field {} or Y = {} or ex b₁ being set st
( b₁ in Y & {} -Seg b₁ misses Y ) )
assume that
A4: Y c= field {} and
A5: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & {} -Seg b₁ misses Y )
thus ex b₁ being set st
( b₁ in Y & {} -Seg b₁ misses Y ) by A4, A5; :: thesis: verum