theorem Th16: :: LATTICE3:16

for N being antisymmetric with_infima RelStr
for n1, n2, n3 being Element of N st N is transitive holds
(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)