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

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