theorem :: RELAT_2:30

for R being Relation holds
( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) )