theorem Th14: :: AOFA_A00:19

for a1, a2, a3, a4 being object st a1 <> a2 & a1 <> a3 & a1 <> a4 & a2 <> a3 & a2 <> a4 & a3 <> a4 holds
<*a1,a2,a3,a4*> is one-to-one