let A be limit_ordinal infinite Ordinal; :: thesis: ( [#] A is closed & [#] A is unbounded )
thus [#] A is closed :: thesis: [#] A is unbounded

proof

let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis: ( B in A & sup (([#] A) /\ B) = B implies B in [#] A )
assume A1: B in A ; :: thesis: ( not sup (([#] A) /\ B) = B or B in [#] A )
assume sup (([#] A) /\ B) = B ; :: thesis: B in [#] A
thus B in [#] A by A1; :: thesis: verum

end;

sup ([#] A) = A by ORDINAL2:18;
hence [#] A is unbounded by Def4; :: thesis: verum