let GX be TopSpace; :: thesis: ( [#] GX is connected iff GX is connected )
A1: [#] GX = [#] (GX | ([#] GX)) by PRE_TOPC:def 5;
A2: {} (GX | ([#] GX)) = {} GX ;

A3: now

assume A4: GX is connected ; :: thesis: [#] GX is connected

now

let P1, Q1 be Subset of (GX | ([#] GX)); :: thesis: ( [#] (GX | ([#] GX)) = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} (GX | ([#] GX)) implies Q1 = {} (GX | ([#] GX)) )
assume that
A5: [#] (GX | ([#] GX)) = P1 \/ Q1 and
A6: P1,Q1 are_separated ; :: thesis: ( P1 = {} (GX | ([#] GX)) or Q1 = {} (GX | ([#] GX)) )
reconsider Q = Q1 as Subset of GX by PRE_TOPC:11;
reconsider P = P1 as Subset of GX by PRE_TOPC:11;
P,Q are_separated by A6, Th6;
hence ( P1 = {} (GX | ([#] GX)) or Q1 = {} (GX | ([#] GX)) ) by A2, A1, A4, A5, Def2; :: thesis: verum

end;

then GX | ([#] GX) is connected by Def2;
hence [#] GX is connected by Def3; :: thesis: verum

end;

now

assume [#] GX is connected ; :: thesis: GX is connected
then A7: GX | ([#] GX) is connected by Def3;

now

let P1, Q1 be Subset of GX; :: thesis: ( [#] GX = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} GX implies Q1 = {} GX )
assume that
A8: [#] GX = P1 \/ Q1 and
A9: P1,Q1 are_separated ; :: thesis: ( P1 = {} GX or Q1 = {} GX )
reconsider Q = Q1 as Subset of (GX | ([#] GX)) by A1;
reconsider P = P1 as Subset of (GX | ([#] GX)) by A1;
P,Q are_separated by A1, A8, A9, Th7;
hence ( P1 = {} GX or Q1 = {} GX ) by A2, A1, A7, A8, Def2; :: thesis: verum

end;

hence GX is connected by Def2; :: thesis: verum

end;

hence ( [#] GX is connected iff GX is connected ) by A3; :: thesis: verum