defpred S₁[ set , set ] means ex J being Subset of L st
( $1 = J & $2 = downarrow J );
set R = InclPoset (Ids L);
set P = InclPoset (Ids S);
A1: for I being Element of (InclPoset (Ids S)) ex K being Element of (InclPoset (Ids L)) st S₁[I,K]

let I be Element of (InclPoset (Ids S)); :: thesis:
I in the carrier of (InclPoset (Ids S)) ;
then I in Ids S by YELLOW_1:1;
then I in { X where X is Ideal of S : verum } by WAYBEL_0:def 23;
then consider J being Ideal of S such that
A2: J = I ;
reconsider J = J as non empty directed Subset of L by YELLOW_2:7;
downarrow J in { X where X is Ideal of L : verum } ;
then downarrow J in Ids L by WAYBEL_0:def 23;
then reconsider K = downarrow J as Element of (InclPoset (Ids L)) by YELLOW_1:1;
take K ; :: thesis:
take J ; :: thesis:
thus ( I = J & K = downarrow J ) by A2; :: thesis:

end;

ex f being Function of the carrier of (InclPoset (Ids S)), the carrier of (InclPoset (Ids L)) st
for I being Element of (InclPoset (Ids S)) holds S₁[I,f . I] from FUNCT_2:sch 3(A1);
then consider f being Function of the carrier of (InclPoset (Ids S)), the carrier of (InclPoset (Ids L)) such that
A3: for I being Element of (InclPoset (Ids S)) ex J being Subset of L st
( I = J & f . I = downarrow J ) ;
reconsider f = f as Function of (InclPoset (Ids S)),(InclPoset (Ids L)) ;
take f ; :: thesis:
for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J )

let I be Ideal of S; :: thesis:
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;
then consider J being Subset of L such that
A4: I = J and
A5: f . I = downarrow J by A3;
reconsider J = J as Subset of L ;
take J ; :: thesis:
thus ( I = J & f . I = downarrow J ) by A4, A5; :: thesis:

end;

hence for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J ) ; :: thesis: