for A, B being set
for X being Subset of A
for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )