let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds limpoints X is closed

let X be Subset of A; :: thesis: limpoints X is closed

let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis: ( B in A & sup ((limpoints X) /\ B) = B implies B in limpoints X )

assume B in A ; :: thesis: ( not sup ((limpoints X) /\ B) = B or B in limpoints X )

then reconsider Bl = B as Element of A ;

assume A1: sup ((limpoints X) /\ B) = B ; :: thesis: B in limpoints X

sup (X /\ B) = B

hence B in limpoints X ; :: thesis: verum

let X be Subset of A; :: thesis: limpoints X is closed

let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis: ( B in A & sup ((limpoints X) /\ B) = B implies B in limpoints X )

assume B in A ; :: thesis: ( not sup ((limpoints X) /\ B) = B or B in limpoints X )

then reconsider Bl = B as Element of A ;

assume A1: sup ((limpoints X) /\ B) = B ; :: thesis: B in limpoints X

sup (X /\ B) = B

proof

then
sup (X /\ Bl) = Bl
;
assume
sup (X /\ B) <> B
; :: thesis: contradiction

then consider B1 being Ordinal such that

A2: B1 in B and

A3: X /\ B c= B1 by Th5;

sup ((limpoints X) /\ B) c= sup (succ B1) by A3, Th16, ORDINAL2:22;

then A4: sup ((limpoints X) /\ B) c= succ B1 by ORDINAL2:18;

succ B1 in B by A2, ORDINAL1:28;

then succ B1 in succ B1 by A1, A4;

hence contradiction ; :: thesis: verum

end;then consider B1 being Ordinal such that

A2: B1 in B and

A3: X /\ B c= B1 by Th5;

sup ((limpoints X) /\ B) c= sup (succ B1) by A3, Th16, ORDINAL2:22;

then A4: sup ((limpoints X) /\ B) c= succ B1 by ORDINAL2:18;

succ B1 in B by A2, ORDINAL1:28;

then succ B1 in succ B1 by A1, A4;

hence contradiction ; :: thesis: verum

hence B in limpoints X ; :: thesis: verum