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
A1: a <= a "\/" a by YELLOW_0:22;
a <= a ;
then a "\/" a <= a by YELLOW_0:22;
hence a "\/" a = a by A1, YELLOW_0:def 3; :: thesis: verum