let X, Y be set ; :: thesis: ( X c= Y & Y is subset-closed implies subset-closed_closure_of X c= Y )
assume A1: ( X c= Y & Y is subset-closed ) ; :: thesis: subset-closed_closure_of X c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in subset-closed_closure_of X or x in Y )
reconsider xx = x as set by TARSKI:1;
assume x in subset-closed_closure_of X ; :: thesis: x in Y
then ex y being set st
( xx c= y & y in X ) by Th2;
hence x in Y by A1; :: thesis: verum