theorem AuxEq: :: PREFER_1:47

for X being non empty set
for R being total reflexive Relation of X holds Aux R = (((R ~) `) /\ (R `)) \/ (((R `) ~) /\ ((R `) \/ (R ~)))