defpred S₁[ set ] means $1 is closure Function of L,L;
set h = the closure Function of L,L;
the closure Function of L,L in Funcs ( the carrier of L, the carrier of L) by FUNCT_2:9;
then A1: the closure Function of L,L in the carrier of (MonMaps (L,L)) by YELLOW_1:def 6;
A2: S₁[ the closure Function of L,L] ;
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:58;
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:9;
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