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