defpred S₁[ 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 S₂[ Element of L] means $1 <= sup I;
deffunc H₁( Element of L) -> Element of bool the carrier of L = (downarrow $1) /\ I;
deffunc H₂( 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
( ( S₂[x] implies f . x = H₁(x) ) & ( not S₂[x] implies f . x = H₂(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)) & S₁[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)) & S₁[a,y] ) )
assume a in the carrier of L ; :: thesis: ex y being object st
( y in the carrier of (InclPoset (Ids L)) & S₁[a,y] )
then reconsider x = a as Element of L ;
take y = f . x; :: thesis: ( y in the carrier of (InclPoset (Ids L)) & S₁[a,y] )
thus y in the carrier of (InclPoset (Ids L)) :: thesis: S₁[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 S₁[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
S₁[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 b₁ being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds
( ( x <= sup I implies b₁ . x = (downarrow x) /\ I ) & ( not x <= sup I implies b₁ . x = downarrow x ) ) ; :: thesis: verum