deffunc H_{1}( Element of L) -> Element of bool the carrier of L = R -below $1;

A1: for x being Element of L holds H_{1}(x) is Element of (InclPoset (LOWER L))

A2: for x being Element of L holds f . x = H_{1}(x)
from FUNCT_2:sch 9(A1);

take f ; :: thesis: for x being Element of L holds f . x = R -below x

let x be Element of L; :: thesis: f . x = R -below x

thus f . x = R -below x by A2; :: thesis: verum

A1: for x being Element of L holds H

proof

consider f being Function of L,(InclPoset (LOWER L)) such that
let x be Element of L; :: thesis: H_{1}(x) is Element of (InclPoset (LOWER L))

reconsider I = H_{1}(x) as lower Subset of L ;

LOWER L = { X where X is Subset of L : X is lower } by LATTICE7:def 7;

then I in LOWER L ;

hence H_{1}(x) is Element of (InclPoset (LOWER L))
by YELLOW_1:1; :: thesis: verum

end;reconsider I = H

LOWER L = { X where X is Subset of L : X is lower } by LATTICE7:def 7;

then I in LOWER L ;

hence H

A2: for x being Element of L holds f . x = H

take f ; :: thesis: for x being Element of L holds f . x = R -below x

let x be Element of L; :: thesis: f . x = R -below x

thus f . x = R -below x by A2; :: thesis: verum