deffunc H_{1}( 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_{1}(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_{1}(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)

set P = InclPoset (Ids S);

A1: for I being set st I in the carrier of (InclPoset (Ids S)) holds

H

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

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

hence
for I being Ideal of S holds f . I = "\/" (I,L)
; :: thesis: verum
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;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