defpred S₁[ set , set ] means ex y being Element of L st
( $1 = y & $2 = (waybelow y) /\ B );
set P = InclPoset (Ids (subrelstr B));
A1: for x being Element of L ex z being Element of (InclPoset (Ids (subrelstr B))) st S₁[x,z]

proof

let x be Element of L; :: thesis: ex z being Element of (InclPoset (Ids (subrelstr B))) st S₁[x,z]
reconsider y = x as Element of L ;
A2: the carrier of (subrelstr B) = B by YELLOW_0:def 15;
Bottom L in B by Def8;
then (waybelow y) /\ B is Ideal of (subrelstr B) by A2, Th50;
then reconsider z = (waybelow y) /\ B as Element of (InclPoset (Ids (subrelstr B))) by YELLOW_2:41;
take z ; :: thesis: S₁[x,z]
take y ; :: thesis: ( x = y & z = (waybelow y) /\ B )
thus ( x = y & z = (waybelow y) /\ B ) ; :: thesis: verum

end;

ex f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) st
for x being Element of L holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
then consider f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) such that
A3: for x being Element of L ex y being Element of L st
( x = y & f . x = (waybelow y) /\ B ) ;
reconsider f = f as Function of L,(InclPoset (Ids (subrelstr B))) ;
take f ; :: thesis: for x being Element of L holds f . x = (waybelow x) /\ B

now :: thesis: for x being Element of L holds f . x = (waybelow x) /\ B

let x be Element of L; :: thesis: f . x = (waybelow x) /\ B
ex y being Element of L st
( x = y & f . x = (waybelow y) /\ B ) by A3;
hence f . x = (waybelow x) /\ B ; :: thesis: verum

end;

hence for x being Element of L holds f . x = (waybelow x) /\ B ; :: thesis: verum