let X be set ; :: thesis: for P being Relation holds
( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )
let P be Relation; :: thesis: ( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )
thus ( P is_strongly_connected_in X implies ( P is_reflexive_in X & P is_connected_in X ) ) :: thesis: ( P is_reflexive_in X & P is_connected_in X implies P is_strongly_connected_in X )

proof

assume A1: P is_strongly_connected_in X ; :: thesis: ( P is_reflexive_in X & P is_connected_in X )
thus P is_reflexive_in X :: thesis: P is_connected_in X

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in P )
assume x in X ; :: thesis: [x,x] in P
hence [x,x] in P by A1, RELAT_2:def 7; :: thesis: verum

end;

let x be set ; :: according to RELAT_2:def 6 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or x = b₁ or [x,b₁] in P or [b₁,x] in P )
let y be set ; :: thesis: ( not x in X or not y in X or x = y or [x,y] in P or [y,x] in P )
assume that
A2: x in X and
A3: y in X ; :: thesis: ( x = y or [x,y] in P or [y,x] in P )
thus ( x = y or [x,y] in P or [y,x] in P ) by A1, A2, A3, RELAT_2:def 7; :: thesis: verum

end;

assume that
A4: P is_reflexive_in X and
A5: P is_connected_in X ; :: thesis: P is_strongly_connected_in X
let x be set ; :: according to RELAT_2:def 7 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or [x,b₁] in P or [b₁,x] in P )
let y be set ; :: thesis: ( not x in X or not y in X or [x,y] in P or [y,x] in P )
assume that
A6: x in X and
A7: y in X ; :: thesis: ( [x,y] in P or [y,x] in P )
( x = y & not [x,y] in P implies [y,x] in P ) by A4, A6, RELAT_2:def 1;
hence ( [x,y] in P or [y,x] in P ) by A5, A6, A7, RELAT_2:def 6; :: thesis: verum