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 ORDINAL2:22, XBOOLE_1:17;
then A5: sup (X /\ B) c= B by ORDINAL2:18;
(X \ B1) /\ B c= X /\ B by XBOOLE_1:26, XBOOLE_1:36;
then B c= sup (X /\ B) by A4, ORDINAL2:22;
then sup (X /\ B) = B by A5, XBOOLE_0:def 10;
then A6: B in X by A2, A3;
assume not B in X \ B1 ; :: thesis: contradiction
then B in B1 by A6, XBOOLE_0:def 5;
then A7: B c= B1 by ORDINAL1:def 2;
X \ B misses B by XBOOLE_1:79;
then X \ B1 misses B by A7, XBOOLE_1:34, XBOOLE_1:63;
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 A9, A11;
hence D in X \ B1 by A10, XBOOLE_0:def 5; :: 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 A14, ORDINAL1:5;
hence D in X \ B1 by A13, XBOOLE_0:def 5; :: thesis: B2 c= D
thus B2 c= D by A12, A14; :: thesis: verum

end;

end;

end;

hence X \ B1 is unbounded by Th6; :: thesis: verum