defpred S₁[ set ] means $1 is closure Function of L,L;
consider h being closure Function of L,L;
h in Funcs the carrier of L,the carrier of L by FUNCT_2:12;
then A1: h in the carrier of (MonMaps L,L) by YELLOW_1:def 6;
A2: S₁[h] ;
consider S being non empty strict full SubRelStr of MonMaps L,L such that
A3: for f being Element of (MonMaps L,L) holds
( f is Element of S iff S₁[f] ) from WAYBEL10:sch 1(A2, A1);
take S ; :: thesis: for f being Function of L,L holds
( f is Element of S iff f is closure )
let f be Function of L,L; :: thesis: ( f is Element of S iff f is closure )

hereby :: thesis: ( f is closure implies f is Element of S )

assume A4: f is Element of S ; :: thesis: f is closure
then f is Element of (MonMaps L,L) by YELLOW_0:59;
hence f is closure by A3, A4; :: thesis: verum

end;

assume A5: f is closure ; :: thesis: f is Element of S
f in Funcs the carrier of L,the carrier of L by FUNCT_2:12;
then f in the carrier of (MonMaps L,L) by A5, YELLOW_1:def 6;
hence f is Element of S by A3, A5; :: thesis: verum