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
proof
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 sup (X /\ Bl) = Bl ;
hence B in limpoints X ; :: thesis: verum