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