let R be Relation; :: thesis: ( R is strongly_connected implies ( R is connected & R is reflexive ) )
assume A1: R is_strongly_connected_in field R ; :: according to RELAT_2:def 15 :: thesis: ( R is connected & R is reflexive )
then for x, y being object st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R ;
hence R is connected by Def6; :: thesis: R is reflexive
let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( x in field R implies [x,x] in R )
thus ( x in field R implies [x,x] in R ) by A1; :: thesis: verum