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 )
assume that
A1: P is_reflexive_in X and
A2: P is_connected_in X ; :: thesis: P is_strongly_connected_in X
let x, y be object ; :: according to RELAT_2:def 7 :: thesis: ( not x in X or not y in X or [x,y] in P or [y,x] in P )
assume that
A3: x in X and
A4: 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 A1, A3;
hence ( [x,y] in P or [y,x] in P ) by A2, A3, A4; :: thesis: verum