deffunc H₁( Element of L) -> Element of bool the carrier of L = R -below $1;
A1: for x being Element of L holds H₁(x) is Element of (InclPoset (LOWER L))

proof

let x be Element of L; :: thesis: H₁(x) is Element of (InclPoset (LOWER L))
reconsider I = H₁(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₁(x) is Element of (InclPoset (LOWER L)) by YELLOW_1:1; :: thesis: verum

end;

consider f being Function of L,(InclPoset (LOWER L)) such that
A2: for x being Element of L holds f . x = H₁(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