let X1, X2 be TopSpace; :: thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) holds
Cl D1 c= Cl D2
let D1 be Subset of X1; :: thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) holds
Cl D1 c= Cl D2
let D2 be Subset of X2; :: thesis: ( D1 c= D2 & TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) implies Cl D1 c= Cl D2 )
assume A1: D1 c= D2 ; :: thesis: ( not TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) or Cl D1 c= Cl D2 )
assume A2: TopStruct(# the carrier of X1,the topology of X1 #) = TopStruct(# the carrier of X2,the topology of X2 #) ; :: thesis: Cl D1 c= Cl D2
then reconsider C2 = D1 as Subset of X2 ;
( Cl D1 = Cl C2 & Cl C2 c= Cl D2 ) by A1, A2, Th80, PRE_TOPC:49;
hence Cl D1 c= Cl D2 ; :: thesis: verum