theorem LEM2a: :: PREFER_1:21

for X being set
for R being Relation of X holds R /\ (R ~) is symmetric