let A be Ordinal; :: thesis: RelIncl A is well-ordering
thus ( RelIncl A is reflexive & RelIncl A is transitive & RelIncl A is antisymmetric & RelIncl A is connected & RelIncl A is well_founded ) by Th2, Th3, Th4, Th5, Th6; :: according to WELLORD1:def 4 :: thesis: verum