let GX be TopSpace; :: thesis: ( [#] GX is connected iff GX is connected )

A1: [#] GX = [#] (GX | ([#] GX)) by PRE_TOPC:def 5;

A1: [#] GX = [#] (GX | ([#] GX)) by PRE_TOPC:def 5;

A2: now :: thesis: ( GX is connected implies [#] GX is connected )

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

hence [#] GX is connected ; :: thesis: verum

end;now :: thesis: for P1, Q1 being Subset of (GX | ([#] GX)) st [#] (GX | ([#] GX)) = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} (GX | ([#] GX)) holds

Q1 = {} (GX | ([#] GX))

then
GX | ([#] GX) is connected
;Q1 = {} (GX | ([#] GX))

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

A4: [#] (GX | ([#] GX)) = P1 \/ Q1 and

A5: 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 A5, Th5;

hence ( P1 = {} (GX | ([#] GX)) or Q1 = {} (GX | ([#] GX)) ) by A1, A3, A4; :: thesis: verum

end;assume that

A4: [#] (GX | ([#] GX)) = P1 \/ Q1 and

A5: 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 A5, Th5;

hence ( P1 = {} (GX | ([#] GX)) or Q1 = {} (GX | ([#] GX)) ) by A1, A3, A4; :: thesis: verum

hence [#] GX is connected ; :: thesis: verum

now :: thesis: ( [#] GX is connected implies GX is connected )

hence
( [#] GX is connected iff GX is connected )
by A2; :: thesis: verumassume
[#] GX is connected
; :: thesis: GX is connected

then A6: GX | ([#] GX) is connected ;

end;then A6: GX | ([#] GX) is connected ;

now :: thesis: for P1, Q1 being Subset of GX st [#] GX = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} GX holds

Q1 = {} GX

hence
GX is connected
; :: thesis: verumQ1 = {} GX

let P1, Q1 be Subset of GX; :: thesis: ( [#] GX = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} GX implies Q1 = {} GX )

assume that

A7: [#] GX = P1 \/ Q1 and

A8: 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, A7, A8, Th6;

hence ( P1 = {} GX or Q1 = {} GX ) by A1, A6, A7; :: thesis: verum

end;assume that

A7: [#] GX = P1 \/ Q1 and

A8: 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, A7, A8, Th6;

hence ( P1 = {} GX or Q1 = {} GX ) by A1, A6, A7; :: thesis: verum