Description: A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22Feb2007)
Ref  Expression  

Hypothesis  clscld.1   X = U. J 

Assertion  sscls   ( ( J e. Top /\ S C_ X ) > S C_ ( ( cls ` J ) ` S ) ) 
Step  Hyp  Ref  Expression 

1  clscld.1   X = U. J 

2  ssintub   S C_ ^ { x e. ( Clsd ` J )  S C_ x } 

3  1  clsval   ( ( J e. Top /\ S C_ X ) > ( ( cls ` J ) ` S ) = ^ { x e. ( Clsd ` J )  S C_ x } ) 
4  2 3  sseqtrrid   ( ( J e. Top /\ S C_ X ) > S C_ ( ( cls ` J ) ` S ) ) 