let FT be non empty RelStr ; :: thesis: for C being Subset of FT st FT is reflexive & FT is symmetric & C is connected holds
C ^b is connected
let C be Subset of FT; :: thesis: ( FT is reflexive & FT is symmetric & C is connected implies C ^b is connected )
assume A1: ( FT is reflexive & FT is symmetric & C is connected ) ; :: thesis: C ^b is connected
then C c= C ^b by FIN_TOPO:18;
hence C ^b is connected by A1, Th35; :: thesis: verum