let L be Semilattice; :: thesis: for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
let x, y be Element of L; :: thesis: "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
(downarrow x) /\ (downarrow y) = downarrow (x "/\" y) by WAYBEL14:3;
hence "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y by WAYBEL_0:34; :: thesis: verum