let A be limit_ordinal infinite Ordinal; :: thesis: for B1 being Ordinal
for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )

let B1 be Ordinal; :: thesis: for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )

let X be Subset of A; :: thesis: ( B1 in A & X is closed & X is unbounded implies ( X \ B1 is closed & X \ B1 is unbounded ) )
assume A1: B1 in A ; :: thesis: ( not X is closed or not X is unbounded or ( X \ B1 is closed & X \ B1 is unbounded ) )
assume A2: ( X is closed & X is unbounded ) ; :: thesis: ( X \ B1 is closed & X \ B1 is unbounded )
thus X \ B1 is closed :: thesis: X \ B1 is unbounded
proof
let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis: ( B in A & sup ((X \ B1) /\ B) = B implies B in X \ B1 )
assume A3: B in A ; :: thesis: ( not sup ((X \ B1) /\ B) = B or B in X \ B1 )
assume A4: sup ((X \ B1) /\ B) = B ; :: thesis: B in X \ B1
sup (X /\ B) c= sup B by ;
then A5: sup (X /\ B) c= B by ORDINAL2:18;
(X \ B1) /\ B c= X /\ B by ;
then B c= sup (X /\ B) by ;
then sup (X /\ B) = B by ;
then A6: B in X by A2, A3;
assume not B in X \ B1 ; :: thesis: contradiction
then B in B1 by ;
then A7: B c= B1 by ORDINAL1:def 2;
X \ B misses B by XBOOLE_1:79;
then X \ B1 misses B by ;
then (X \ B1) /\ B = {} by XBOOLE_0:def 7;
hence contradiction by A4, ORDINAL2:18; :: thesis: verum
end;
for B2 being Ordinal st B2 in A holds
ex C being Ordinal st
( C in X \ B1 & B2 c= C )
proof
let B2 be Ordinal; :: thesis: ( B2 in A implies ex C being Ordinal st
( C in X \ B1 & B2 c= C ) )

assume A8: B2 in A ; :: thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )

per cases ( B1 in B2 or B2 c= B1 ) by ORDINAL1:16;
suppose A9: B1 in B2 ; :: thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )

consider D being Ordinal such that
A10: D in X and
A11: B2 c= D by A2, A8, Th6;
take D ; :: thesis: ( D in X \ B1 & B2 c= D )
B1 in D by ;
hence D in X \ B1 by ; :: thesis: B2 c= D
thus B2 c= D by A11; :: thesis: verum
end;
suppose A12: B2 c= B1 ; :: thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )

consider D being Ordinal such that
A13: D in X and
A14: B1 c= D by A1, A2, Th6;
take D ; :: thesis: ( D in X \ B1 & B2 c= D )
not D in B1 by ;
hence D in X \ B1 by ; :: thesis: B2 c= D
thus B2 c= D by ; :: thesis: verum
end;
end;
end;
hence X \ B1 is unbounded by Th6; :: thesis: verum