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 )
assume A1: X c= A ; :: thesis: RelIncl X is well-ordering
(RelIncl A) |_2 X is well-ordering by Th7, WELLORD1:32;
hence RelIncl X is well-ordering by A1, Th8; :: thesis: verum