let X be non empty TopSpace; :: thesis: for Y0 being SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let Y0 be SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let C, A be Subset of X; :: thesis: for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let B be Subset of Y0; :: thesis: ( C is closed & C c= the carrier of Y0 & A c= C & A = B implies Cl A = Cl B )
assume A1: C is closed ; :: thesis: ( not C c= the carrier of Y0 or not A c= C or not A = B or Cl A = Cl B )
assume A2: C c= the carrier of Y0 ; :: thesis: ( not A c= C or not A = B or Cl A = Cl B )
assume A c= C ; :: thesis: ( not A = B or Cl A = Cl B )
then Cl A c= Cl C by PRE_TOPC:19;
then Cl A c= C by A1, PRE_TOPC:22;
then A3: Cl A = (Cl A) /\ ([#] Y0) by A2, XBOOLE_1:1, XBOOLE_1:28;
assume A = B ; :: thesis: Cl A = Cl B
hence Cl A = Cl B by A3, PRE_TOPC:17; :: thesis: verum