for A, B being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B & (R ~) .: (R .: A) = (R ~) .: (proj2 R) ) by Th50;