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