theorem :: RELAT_2:28

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