let G be non empty TopSpace; :: thesis: for P, A being Subset of G
for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
let P, A be Subset of G; :: thesis: for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
let Q be Subset of (G | A); :: thesis: ( P = Q & P is connected implies Q is connected )
assume that
A1: P = Q and
A2: P is connected ; :: thesis: Q is connected
A3: G | P is connected by A2;
Q c= the carrier of (G | A) ;
then Q c= A by PRE_TOPC:8;
then G | P = (G | A) | Q by A1, PRE_TOPC:7;
hence Q is connected by A3; :: thesis: verum