let A be limit_ordinal infinite Ordinal; :: thesis:
let B1 be Ordinal; :: thesis:
let X be Subset of A; :: thesis:
assume A1: B1 in A ; :: thesis:
assume A2: ( X is closed & X is unbounded ) ; :: thesis:
thus X \ B1 is closed :: thesis:

let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis:
assume A3: B in A ; :: thesis:
assume A4: sup ((X \ B1) /\ B) = B ; :: thesis:
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:
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:

end;

for B2 being Ordinal st B2 in A holds
ex C being Ordinal st
( C in X \ B1 & B2 c= C )

let B2 be Ordinal; :: thesis:
assume A8: B2 in A ; :: thesis:

per cases by ORDINAL1:16;

suppose A9: B1 in B2 ; :: thesis:

consider D being Ordinal such that
A10: D in X and
A11: B2 c= D by A2, A8, Th6;
take D ; :: thesis:
B1 in D by A9, A11;
hence D in X \ B1 by A10, XBOOLE_0:def 5; :: thesis:
thus B2 c= D by A11; :: thesis:

end;

suppose A12: B2 c= B1 ; :: thesis:

consider D being Ordinal such that
A13: D in X and
A14: B1 c= D by A1, A2, Th6;
take D ; :: thesis:
not D in B1 by A14, ORDINAL1:5;
hence D in X \ B1 by A13, XBOOLE_0:def 5; :: thesis:
thus B2 c= D by A12, A14; :: thesis:

end;

end;

end;

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