let L be trivial Semilattice; :: thesis: L is modular
let a, b, c be Element of L; :: according to YELLOW11:def 3 :: thesis: ( not a <= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume a <= c ; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
thus a "\/" (b "/\" c) = (a "\/" b) "/\" c by STRUCT_0:def 10; :: thesis: verum