let T be non empty TopSpace; :: thesis: for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) holds
A = Cl B
let A, B be Subset of T; :: thesis: ( B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) implies A = Cl B )
assume that
A1: ( B c= A & A is closed ) and
A2: for C being Subset of T st B c= C & C is closed holds
A c= C ; :: thesis: A = Cl B
thus A c= Cl B by A2, PRE_TOPC:18; :: according to XBOOLE_0:def 10 :: thesis: Cl B c= A
thus Cl B c= A by A1, TOPS_1:5; :: thesis: verum