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 that
A1: ( FT is reflexive & FT is symmetric ) and
A2: C is connected ; :: thesis: C ^b is connected
C c= C ^b by A1, FIN_TOPO:18;
hence C ^b is connected by A1, A2, Th35; :: thesis: verum