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