let FT be non empty RelStr ; :: thesis: for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds
for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S )
let C be Subset of FT; :: thesis: ( FT is filled & FT is symmetric & C is connected implies for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S ) )
assume A1: ( FT is filled & FT is symmetric & C is connected ) ; :: thesis: for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S )
let S be Subset of FT; :: thesis: ( not S is_a_component_of FT or C misses S or C c= S )
assume A2: S is_a_component_of FT ; :: 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;
then C \/ S is connected by A1, A4, Th33, FINTOPO4:6;
then S = C \/ S by A2, A3;
hence C c= S by XBOOLE_1:7; :: thesis: verum