deffunc H₁( Element of L) -> Subset of L = AR -below $1;
A1: for x being Element of L holds H₁(x) is Element of (InclPoset (Ids L))

proof

let x be Element of L; :: thesis: H₁(x) is Element of (InclPoset (Ids L))
reconsider I = H₁(x) as Ideal of L ;
I in Ids L ;
hence H₁(x) is Element of (InclPoset (Ids L)) by YELLOW_1:1; :: thesis: verum

end;

consider f being Function of L,(InclPoset (Ids 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 = AR -below x
thus for x being Element of L holds f . x = AR -below x by A2; :: thesis: verum