let R be Relation; :: thesis: ( R is strongly_connected implies ( R is connected & R is reflexive ) )
assume R is strongly_connected ; :: thesis: ( R is connected & R is reflexive )
then A1: R is_strongly_connected_in field R by Def15;
then for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R by Def7;
then R is_connected_in field R by Def6;
hence R is connected by Def14; :: thesis: R is reflexive
thus R is reflexive :: thesis: verum

proof

let x be set ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( x in field R implies [x,x] in R )
assume x in field R ; :: thesis: [x,x] in R
hence [x,x] in R by A1, Def7; :: thesis: verum

end;