let L be sup-Semilattice; :: thesis: for x, y being Element of L holds "/\" ((uparrow x) /\ (uparrow y)),L = x "\/" y
let x, y be Element of L; :: thesis: "/\" ((uparrow x) /\ (uparrow y)),L = x "\/" y
(uparrow x) /\ (uparrow y) = uparrow (x "\/" y) by WAYBEL14:4;
hence "/\" ((uparrow x) /\ (uparrow y)),L = x "\/" y by WAYBEL_0:39; :: thesis: verum