defpred S_{1}[ 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_{1}[ 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_{1}[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 )

f is Element of (ClOpers L) by Def1;

hence f is Element of S by A3, A5; :: thesis: verum

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

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

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 A5:
f is directed-sups-preserving
; :: thesis: f is Element of Sassume 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;then f is Element of (ClOpers L) by YELLOW_0:58;

hence f is directed-sups-preserving by A3, A4; :: thesis: verum

f is Element of (ClOpers L) by Def1;

hence f is Element of S by A3, A5; :: thesis: verum