let A be Ordinal; :: thesis: for X being set st X c= A holds

RelIncl X is well-ordering

let X be set ; :: thesis: ( X c= A implies RelIncl X is well-ordering )

(RelIncl A) |_2 X is well-ordering by WELLORD1:25;

hence ( X c= A implies RelIncl X is well-ordering ) by Th1; :: thesis: verum

RelIncl X is well-ordering

let X be set ; :: thesis: ( X c= A implies RelIncl X is well-ordering )

(RelIncl A) |_2 X is well-ordering by WELLORD1:25;

hence ( X c= A implies RelIncl X is well-ordering ) by Th1; :: thesis: verum