let FT be non empty RelStr ; :: thesis: for A being Subset of FT st FT is reflexive & FT is symmetric & A is_a_component_of FT holds
A is closed
let A be Subset of FT; :: thesis: ( FT is reflexive & FT is symmetric & A is_a_component_of FT implies A is closed )
assume that
A1: ( FT is reflexive & FT is symmetric ) and
A2: A is_a_component_of FT ; :: thesis: A is closed
A is connected by A2, Def4;
then A3: A ^b is connected by A1, Th36;
A c= A ^b by A1, FIN_TOPO:18;
hence A = A ^b by A2, A3, Def4; :: according to FIN_TOPO:def 17 :: thesis: verum