theorem Th15: :: LATTICE3:15

for N being antisymmetric with_infima RelStr
for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1