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