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 b <= a ; :: thesis: a "/\" b = b
then b "/\" b <= a "/\" b by Th6;
then ( a "/\" b <= b & b <= a "/\" b ) by Th2, YELLOW_0:23;
hence a "/\" b = b by YELLOW_0:def 3; :: thesis: verum