defpred S₁[ object , object ] means ex AR being auxiliary Relation of L st
( AR = $1 & $2 = AR -below );
A1: for a being object st a in the carrier of (InclPoset (Aux L)) holds
ex y being object st
( y in the carrier of (MonSet L) & S₁[a,y] )

proof

let a be object ; :: thesis: ( a in the carrier of (InclPoset (Aux L)) implies ex y being object st
( y in the carrier of (MonSet L) & S₁[a,y] ) )
assume a in the carrier of (InclPoset (Aux L)) ; :: thesis: ex y being object st
( y in the carrier of (MonSet L) & S₁[a,y] )
then a in Aux L by YELLOW_1:1;
then reconsider AR = a as auxiliary Relation of L by Def8;
take AR -below ; :: thesis: ( AR -below in the carrier of (MonSet L) & S₁[a,AR -below ] )
thus ( AR -below in the carrier of (MonSet L) & S₁[a,AR -below ] ) by Th18; :: thesis: verum

end;

consider f being Function of the carrier of (InclPoset (Aux L)), the carrier of (MonSet L) such that
A2: for a being object st a in the carrier of (InclPoset (Aux L)) holds
S₁[a,f . a] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for AR being auxiliary Relation of L holds f . AR = AR -below

now :: thesis: for AR being auxiliary Relation of L holds f . AR = AR -below

let AR be auxiliary Relation of L; :: thesis: f . AR = AR -below
AR in Aux L by Def8;
then AR in the carrier of (InclPoset (Aux L)) by YELLOW_1:1;
then S₁[AR,f . AR] by A2;
hence f . AR = AR -below ; :: thesis: verum

end;

hence for AR being auxiliary Relation of L holds f . AR = AR -below ; :: thesis: verum