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

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