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

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