deffunc H_{1}( Element of L, Element of L) -> Element of the carrier of L = $1 "/\" $2;

A1: for x, y being Element of L holds H_{1}(x,y) is Element of L
;

consider f being Function of [:L,L:],L such that

A2: for x, y being Element of L holds f . (x,y) = H_{1}(x,y)
from YELLOW_3:sch 6(A1);

take f ; :: thesis: for x, y being Element of L holds f . (x,y) = x "/\" y

thus for x, y being Element of L holds f . (x,y) = x "/\" y by A2; :: thesis: verum

A1: for x, y being Element of L holds H

consider f being Function of [:L,L:],L such that

A2: for x, y being Element of L holds f . (x,y) = H

take f ; :: thesis: for x, y being Element of L holds f . (x,y) = x "/\" y

thus for x, y being Element of L holds f . (x,y) = x "/\" y by A2; :: thesis: verum