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

proof

let I be Ideal of S; :: thesis: f . I = "\/" (I,L)
I in { X where X is Ideal of S : verum } ;
then I in the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by WAYBEL_0:def 23;
then I in the carrier of (InclPoset (Ids S)) by YELLOW_1:def 1;
hence f . I = "\/" (I,L) by A2; :: thesis: verum

end;

hence for I being Ideal of S holds f . I = "\/" (I,L) ; :: thesis: verum