let GX be TopSpace; :: thesis: for P1, P being Subset of GX
for Q9 being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
let P1, P be Subset of GX; :: thesis: for Q9 being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
let Q9 be Subset of (GX | P1); :: thesis: for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
let Q be Subset of (GX | P); :: thesis: ( P1 c= P & Q = Q9 & Q9 is connected implies Q is connected )
assume that
A1: P1 c= P and
A2: Q = Q9 and
A3: Q9 is connected ; :: thesis: Q is connected
[#] (GX | P) = P by PRE_TOPC:def 5;
then reconsider P19 = P1 as Subset of (GX | P) by A1;
GX | P1 = (GX | P) | P19 by A1, PRE_TOPC:7;
hence Q is connected by A2, A3, CONNSP_1:23; :: thesis: verum