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 )
A3: 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 A4: 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:26;

suppose A5: B1 in B2 ; :: thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )

consider D being Ordinal such that
A6: D in X and
A7: B2 c= D by A2, A4, Th7;
take D ; :: thesis: ( D in X \ B1 & B2 c= D )
B1 in D by A5, A7;
hence D in X \ B1 by A6, XBOOLE_0:def 5; :: thesis: B2 c= D
thus B2 c= D by A7; :: thesis: verum

end;

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

consider D being Ordinal such that
A9: D in X and
A10: B1 c= D by A1, A2, Th7;
take D ; :: thesis: ( D in X \ B1 & B2 c= D )
not D in B1 by A10, ORDINAL1:7;
hence D in X \ B1 by A9, XBOOLE_0:def 5; :: thesis: B2 c= D
thus B2 c= D by A8, A10, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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 A11: B in A ; :: thesis: ( not sup ((X \ B1) /\ B) = B or B in X \ B1 )
assume A12: sup ((X \ B1) /\ B) = B ; :: thesis: B in X \ B1
sup (X /\ B) = B

proof

(X \ B1) /\ B c= X /\ B by XBOOLE_1:26, XBOOLE_1:36;
then A13: B c= sup (X /\ B) by A12, ORDINAL2:30;
sup (X /\ B) c= sup B by ORDINAL2:30, XBOOLE_1:17;
then sup (X /\ B) c= B by ORDINAL2:26;
hence sup (X /\ B) = B by A13, XBOOLE_0:def 10; :: thesis: verum

end;

then A14: B in X by A2, A11, Def5;
assume not B in X \ B1 ; :: thesis: contradiction
then B in B1 by A14, XBOOLE_0:def 5;
then A15: B c= B1 by ORDINAL1:def 2;
X \ B misses B by XBOOLE_1:79;
then X \ B1 misses B by A15, XBOOLE_1:34, XBOOLE_1:63;
then (X \ B1) /\ B = {} by XBOOLE_0:def 7;
hence contradiction by A12, ORDINAL2:26; :: thesis: verum

end;

thus X \ B1 is unbounded by A3, Th7; :: thesis: verum