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_of GX 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_of GX 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_of GX or C misses S or C c= S )
let S be Subset of GX; :: thesis: ( not S is_a_component_of GX or C misses S or C c= S )
assume A2: S is_a_component_of GX ; :: thesis: ( C misses S or C c= S )
A3: S c= C \/ S by XBOOLE_1:7;
assume A4: C meets S ; :: thesis: C c= S
S is connected by A2, Def5;
then C \/ S is connected by A1, A4, Th2, Th18;
then S = C \/ S by A2, A3, Def5;
hence C c= S by XBOOLE_1:7; :: thesis: verum