deffunc H₁( Element of ) -> Subset of = AR -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 Ideal of L ;
I in Ids L ;
hence H₁(x) is Element of by YELLOW_1:1; :: thesis: verum

end;

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