let X be set ; :: thesis: ( subset-closed_closure_of X c= X implies X is subset-closed )
set f = subset-closed_closure_of X;
assume A1: subset-closed_closure_of X c= X ; :: thesis: X is subset-closed
let x be set ; :: according to CLASSES1:def 1 :: thesis: for b₁ being set holds
( not x in X or not b₁ c= x or b₁ in X )
let y be set ; :: thesis: ( not x in X or not y c= x or y in X )
assume ( x in X & y c= x ) ; :: thesis: y in X
then y in subset-closed_closure_of X by Th2;
hence y in X by A1; :: thesis: verum