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

proof

let x be Element of ; :: thesis: H₁(x) is Element of
reconsider I = H₁(x) as lower Subset of ;
LOWER L = { X where X is Subset of : X is lower } by LATTICE7:def 7;
then I in LOWER L ;
hence H₁(x) is Element of by YELLOW_1:1; :: thesis: verum

end;

consider f being Function of L,(InclPoset (LOWER L)) such that
A2: for x being Element of holds f . x = H₁(x) from FUNCT_2:sch 9(A1);
take f ; :: thesis: for x being Element of holds f . x = R -below x
let x be Element of ; :: thesis: f . x = R -below x
thus f . x = R -below x by A2; :: thesis: verum