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 X is_club_in A ; :: thesis: ( X is closed & X is unbounded )
then ( X is_closed_in A & X is_unbounded_in A ) by Def3;
then ( ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) & sup X = A ) by Def1, Def2;
hence ( X is closed & X is unbounded ) by Def4, Def5; :: thesis: verum

end;

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