let V be antisymmetric with_suprema RelStr ; :: thesis: for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1
let u1, u2 be Element of V; :: thesis: u1 "\/" u2 = u2 "\/" u1
A1: u1 <= u1 "\/" u2 by Lm1;
A2: u2 <= u1 "\/" u2 by Lm1;
for u3 being Element of V st u2 <= u3 & u1 <= u3 holds
u1 "\/" u2 <= u3 by Lm1;
hence u1 "\/" u2 = u2 "\/" u1 by A1, A2, Def13; :: thesis: verum