theorem Lemma9: :: PREFER_1:27

for a, b being object st a <> b holds
( {[a,b],[b,a]} is irreflexive & {[a,b],[b,a]} is symmetric )