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

ex C being Ordinal st

( C in X \ B1 & B2 c= C )

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

for B2 being Ordinal st B2 in A holds
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;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

ex C being Ordinal st

( C in X \ B1 & B2 c= C )

proof

hence
X \ B1 is unbounded
by Th6; :: thesis: verum
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 )

end;( 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;

end;

suppose A9:
B1 in B2
; :: thesis: ex C being Ordinal st

( C in X \ B1 & B2 c= C )

( 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;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

suppose A12:
B2 c= B1
; :: thesis: ex C being Ordinal st

( C in X \ B1 & B2 c= C )

( 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;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