defpred S_{1}[ 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_{1}[I,K]

for I being Element of (InclPoset (Ids S)) holds S_{1}[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 )

for I being Ideal of S ex J being Subset of L st

( I = J & f . I = downarrow J )

( I = J & f . I = downarrow J ) ; :: thesis: verum

( $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

proof

ex f being Function of the carrier of (InclPoset (Ids S)), the carrier of (InclPoset (Ids L)) st
let I be Element of (InclPoset (Ids S)); :: thesis: ex K being Element of (InclPoset (Ids L)) st S_{1}[I,K]

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: S_{1}[I,K]

take J ; :: thesis: ( I = J & K = downarrow J )

thus ( I = J & K = downarrow J ) by A2; :: thesis: verum

end;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: S

take J ; :: thesis: ( I = J & K = downarrow J )

thus ( I = J & K = downarrow J ) by A2; :: thesis: verum

for I being Element of (InclPoset (Ids S)) holds S

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 )

for I being Ideal of S ex J being Subset of L st

( I = J & f . I = downarrow J )

proof

hence
for I being Ideal of S ex J being Subset of L st
let I be Ideal of S; :: thesis: ex J being Subset of L st

( I = J & f . I = downarrow J )

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: ( I = J & f . I = downarrow J )

thus ( I = J & f . I = downarrow J ) by A4, A5; :: thesis: verum

end;( I = J & f . I = downarrow J )

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: ( I = J & f . I = downarrow J )

thus ( I = J & f . I = downarrow J ) by A4, A5; :: thesis: verum

( I = J & f . I = downarrow J ) ; :: thesis: verum