deffunc H1( 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
H1(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 = H1(I) from 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