defpred S1[ object , object ] means for x being Element of L st x = $1 holds
( ( x <= sup I implies $2 = (downarrow x) /\ I ) & ( not x <= sup I implies $2 = downarrow x ) );
defpred S2[ Element of L] means $1 <= sup I;
deffunc H1( Element of L) -> Element of bool the carrier of L = (downarrow $1) /\ I;
deffunc H2( Element of L) -> Element of bool the carrier of L = downarrow $1;
consider f being Function such that
A1: ( dom f = the carrier of L & ( for x being Element of L holds
( ( S2[x] implies f . x = H1(x) ) & ( not S2[x] implies f . x = H2(x) ) ) ) ) from PARTFUN1:sch 4();
 A2: for a being object st a in the carrier of L holds
ex y being object st
( y in the carrier of (InclPoset (Ids L)) & S1[a,y] )
proof
let a be object ; :: thesis: ( a in the carrier of L implies ex y being object st
( y in the carrier of (InclPoset (Ids L)) & S1[a,y] ) )
assume a in the carrier of L ; :: thesis: ex y being object st
( y in the carrier of (InclPoset (Ids L)) & S1[a,y] )
then reconsider x = a as Element of L ;
take y = f . x; :: thesis: ( y in the carrier of (InclPoset (Ids L)) & S1[a,y] )
thus y in the carrier of (InclPoset (Ids L)) :: thesis: S1[a,y]
proof
per cases ( x <= sup I or not x <= sup I ) ;
suppose x <= sup I ; :: thesis: y in the carrier of (InclPoset (Ids L))
then y = (downarrow x) /\ I by A1;
then y is Ideal of L by YELLOW_2:40;
then y in { X where X is Ideal of L : verum } ;
hence y in the carrier of (InclPoset (Ids L)) by YELLOW_1:1; :: thesis: verum
end;
suppose not x <= sup I ; :: thesis: y in the carrier of (InclPoset (Ids L))
then y = downarrow x by A1;
then y in { X where X is Ideal of L : verum } ;
hence y in the carrier of (InclPoset (Ids L)) by YELLOW_1:1; :: thesis: verum
end;
end;
end;
thus S1[a,y] by A1; :: thesis: verum
end;
consider f being Function of the carrier of L, the carrier of (InclPoset (Ids L)) such that
A3: for a being object st a in the carrier of L holds
S1[a,f . a] from FUNCT_2:sch 1(A2);
 reconsider f = f as Function of L,(InclPoset (Ids L)) ;
for x being Element of L holds
( ( x <= sup I implies f . x = (downarrow x) /\ I ) & ( not x <= sup I implies f . x = downarrow x ) ) by A3;
hence ex b1 being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds
( ( x <= sup I implies b1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b1 . x = downarrow x ) ) ; :: thesis: verum