let A be limit_ordinal infinite Ordinal; :: thesis: for B1 being Ordinal
for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
let B1 be Ordinal; :: thesis: for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
let X be Subset of A; :: thesis: ( X c= B1 implies limpoints X c= succ B1 )
A1: X /\ A = X by XBOOLE_1:28;
assume X c= B1 ; :: thesis: limpoints X c= succ B1
then A /\ (limpoints X) c= succ B1 by A1, Th16;
hence limpoints X c= succ B1 by XBOOLE_1:28; :: thesis: verum