let L be sup-Semilattice; :: thesis: for a, b being Element of L st a <= b holds
a "\/" b = b
let a, b be Element of L; :: thesis: ( a <= b implies a "\/" b = b )
A1: b <= b ;
assume a <= b ; :: thesis: a "\/" b = b
then ( b <= a "\/" b & a "\/" b <= b ) by A1, YELLOW_0:22;
hence a "\/" b = b by YELLOW_0:def 3; :: thesis: verum