let GX be TopSpace; :: thesis: ( [#] GX is connected iff GX is connected )
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
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))
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;
then GX | ([#] GX) is connected ;
hence [#] GX is connected ; :: thesis: verum
end;
now :: thesis: ( [#] GX is connected implies GX is connected )
assume [#] GX is connected ; :: thesis: GX is connected
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
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;
hence GX is connected ; :: thesis: verum
end;
hence ( [#] GX is connected iff GX is connected ) by A2; :: thesis: verum