let A be limit_ordinal infinite Ordinal; :: thesis: for B1 being Ordinal st B1 in A holds
( A \ B1 is closed & A \ B1 is unbounded )
let B1 be Ordinal; :: thesis: ( B1 in A implies ( A \ B1 is closed & A \ B1 is unbounded ) )
assume A1: B1 in A ; :: thesis: ( A \ B1 is closed & A \ B1 is unbounded )
( [#] A is closed & [#] A is unbounded ) by Th10;
hence ( A \ B1 is closed & A \ B1 is unbounded ) by A1, Th11; :: thesis: verum