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