for X being set
for P being Relation holds
( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )