let GX be TopSpace; :: thesis: for C being Subset of GX st C is connected holds

for S being Subset of GX holds

( not S is a_component or C misses S or C c= S )

let C be Subset of GX; :: thesis: ( C is connected implies for S being Subset of GX holds

( not S is a_component or C misses S or C c= S ) )

assume A1: C is connected ; :: thesis: for S being Subset of GX holds

( not S is a_component or C misses S or C c= S )

let S be Subset of GX; :: thesis: ( not S is a_component or C misses S or C c= S )

assume A2: S is a_component ; :: thesis: ( C misses S or C c= S )

A3: S c= C \/ S by XBOOLE_1:7;

assume C meets S ; :: thesis: C c= S

then C \/ S is connected by A1, A2, Th1, Th17;

then S = C \/ S by A2, A3;

hence C c= S by XBOOLE_1:7; :: thesis: verum

for S being Subset of GX holds

( not S is a_component or C misses S or C c= S )

let C be Subset of GX; :: thesis: ( C is connected implies for S being Subset of GX holds

( not S is a_component or C misses S or C c= S ) )

assume A1: C is connected ; :: thesis: for S being Subset of GX holds

( not S is a_component or C misses S or C c= S )

let S be Subset of GX; :: thesis: ( not S is a_component or C misses S or C c= S )

assume A2: S is a_component ; :: thesis: ( C misses S or C c= S )

A3: S c= C \/ S by XBOOLE_1:7;

assume C meets S ; :: thesis: C c= S

then C \/ S is connected by A1, A2, Th1, Th17;

then S = C \/ S by A2, A3;

hence C c= S by XBOOLE_1:7; :: thesis: verum