theorem Th1: :: WAYBEL16:1
for L being sup-Semilattice
for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y