theorem :: WAYBEL16:2
for L being Semilattice
for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y