let GX be TopSpace; :: thesis: for P1, P being Subset of GX
for Q' being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q' & Q' is connected holds
Q is connected
let P1, P be Subset of GX; :: thesis: for Q' being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q' & Q' is connected holds
Q is connected
let Q' be Subset of (GX | P1); :: thesis: for Q being Subset of (GX | P) st P1 c= P & Q = Q' & Q' is connected holds
Q is connected
let Q be Subset of (GX | P); :: thesis: ( P1 c= P & Q = Q' & Q' is connected implies Q is connected )
assume A1: ( P1 c= P & Q = Q' & Q' is connected ) ; :: thesis: Q is connected
[#] (GX | P) = P by PRE_TOPC:def 10;
then reconsider P1' = P1 as Subset of (GX | P) by A1;
GX | P1 = (GX | P) | P1' by A1, PRE_TOPC:28;
hence Q is connected by A1, CONNSP_1:24; :: thesis: verum