deffunc H₁( set ) -> Element of the carrier of L = "\/" ($1,L);
set P = InclPoset (Ids L);
A1: for I being set st I in the carrier of (InclPoset (Ids L)) holds
H₁(I) in the carrier of L ;
ex f being Function of the carrier of (InclPoset (Ids L)), the carrier of L st
for I being set st I in the carrier of (InclPoset (Ids L)) holds
f . I = H₁(I) from FUNCT_2:sch 11(A1);
then consider f being Function of the carrier of (InclPoset (Ids L)), the carrier of L such that
A2: for I being set st I in the carrier of (InclPoset (Ids L)) holds
f . I = "\/" (I,L) ;
reconsider f = f as Function of (InclPoset (Ids L)),L ;
take f ; :: thesis: for I being Ideal of L holds f . I = sup I
for I being Ideal of L holds f . I = sup I

proof

let I be Ideal of L; :: thesis: f . I = sup I
I in the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) ;
then I in the carrier of (InclPoset (Ids L)) by YELLOW_1:def 1;
hence f . I = sup I by A2; :: thesis: verum

end;

hence for I being Ideal of L holds f . I = sup I ; :: thesis: verum