theorem LEM3b: :: PREFER_1:26
for X being non empty set
for R being total reflexive Relation of X holds R /\ (R ~) is total