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

( 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