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] )

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

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:

end;