let N be antisymmetric with_infima RelStr ; :: thesis: for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1
let n1, n2 be Element of N; :: thesis: n1 "/\" n2 = n2 "/\" n1
A1: n1 "/\" n2 <= n1 by Lm2;
A2: n1 "/\" n2 <= n2 by Lm2;
for n3 being Element of N st n3 <= n2 & n3 <= n1 holds
n3 <= n1 "/\" n2 by Lm2;
hence n1 "/\" n2 = n2 "/\" n1 by A1, A2, Def14; :: thesis: verum