defpred S₁[ set ] means $1 is directed-sups-preserving Function of L,L;
set h = the directed-sups-preserving closure Function of L,L;
the directed-sups-preserving closure Function of L,L is Element of (ClOpers L) by Def1;
then A1: the directed-sups-preserving closure Function of L,L in the carrier of (ClOpers L) ;
A2: S₁[ the directed-sups-preserving closure Function of L,L] ;
consider S being non empty strict full SubRelStr of ClOpers L such that
A3: for f being Element of (ClOpers L) holds
( f is Element of S iff S₁[f] ) from WAYBEL10:sch 1(A2, A1);
take S ; :: thesis: for f being closure Function of L,L holds
( f is Element of S iff f is directed-sups-preserving )
let f be closure Function of L,L; :: thesis: ( f is Element of S iff f is directed-sups-preserving )

hereby :: thesis: ( f is directed-sups-preserving implies f is Element of S )

assume A4: f is Element of S ; :: thesis: f is directed-sups-preserving
then f is Element of (ClOpers L) by YELLOW_0:58;
hence f is directed-sups-preserving by A3, A4; :: thesis: verum

end;

assume A5: f is directed-sups-preserving ; :: thesis: f is Element of S
f is Element of (ClOpers L) by Def1;
hence f is Element of S by A3, A5; :: thesis: verum