let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )
let X be Subset of A; :: thesis: ( X is_club_in A iff ( X is closed & X is unbounded ) )
thus ( X is_club_in A implies ( X is closed & X is unbounded ) ) :: thesis: ( X is closed & X is unbounded implies X is_club_in A )

proof

assume A1: X is_club_in A ; :: thesis: ( X is closed & X is unbounded )
then X is_unbounded_in A by Def3;
then A2: sup X = A by Def1;
X is_closed_in A by A1, Def3;
then for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X by Def2;
hence ( X is closed & X is unbounded ) by A2, Def4, Def5; :: thesis: verum

end;

assume A3: ( X is closed & X is unbounded ) ; :: thesis: X is_club_in A
then sup X = A by Def4;
then A4: X is_unbounded_in A by Def1;
for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X by A3, Def5;
then X is_closed_in A by Def2;
hence X is_club_in A by A4, Def3; :: thesis: verum