theorem ConField: :: PREFER_1:34

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