deffunc H1( Element of L) -> Element of bool the carrier of L = R -below $1;
A1: for x being Element of L holds H1(x) is Element of (InclPoset (LOWER L))
proof
let x be Element of L; :: thesis: H1(x) is Element of (InclPoset (LOWER L))
reconsider I = H1(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 H1(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 = H1(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