let L be reflexive antisymmetric with_suprema RelStr ; :: thesis: for a being Element of L holds a "\/" a = a
let a be Element of L; :: thesis: a "\/" a = a
a <= a ;
then ( a <= a "\/" a & a "\/" a <= a ) by YELLOW_0:22;
hence a "\/" a = a by YELLOW_0:def 3; :: thesis: verum