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 & u2 <= u1 "\/" u2 & ( for u3 being Element of V st u1 <= u3 & u2 <= u3 holds
u1 "\/" u2 <= u3 ) ) 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, Def13; :: thesis: verum