theorem :: ROUGHS_5:37

for R being non empty RelStr holds
( (f_0 R) * (f_0 R) = f_0 R iff (Flip (f_0 R)) * (Flip (f_0 R)) = Flip (f_0 R) )