let FT be non empty RelStr ; :: thesis: for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds
C ^b is connected
let C be Subset of FT; :: thesis: ( FT is filled & FT is symmetric & C is connected implies C ^b is connected )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: C is connected ; :: thesis: C ^b is connected
C c= C ^b by A1, FIN_TOPO:13;
hence C ^b is connected by A1, A2, Th34; :: thesis: verum