:: deftheorem defines Aux PREFER_1:def 10 :
for X being set
for R being Relation of X holds Aux R = SymCl ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `);