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

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