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

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