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 A1: B in A ; :: thesis: ( not sup ((limpoints X) /\ B) = B or B in limpoints X )
assume A2: sup ((limpoints X) /\ B) = B ; :: thesis: B in limpoints X
A3: sup (X /\ B) = B

proof

assume sup (X /\ B) <> B ; :: thesis: contradiction
then consider B1 being Ordinal such that
A4: B1 in B and
A5: X /\ B c= B1 by Th6;
sup ((limpoints X) /\ B) c= sup (succ B1) by A5, Th17, ORDINAL2:30;
then A6: sup ((limpoints X) /\ B) c= succ B1 by ORDINAL2:26;
succ B1 in B by A4, ORDINAL1:41;
then succ B1 in succ B1 by A2, A6;
hence contradiction ; :: thesis: verum

end;

reconsider Bl = B as Element of A by A1;
( not Bl is finite & Bl is limit_ordinal & sup (X /\ Bl) = Bl ) by A3;
hence B in limpoints X ; :: thesis: verum