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

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