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