defpred S_{1}[ object ] means $1 is directed-sups-preserving closure Function of L,L;

let S1, S2 be non empty strict full SubRelStr of ClOpers L; :: thesis: ( ( for f being closure Function of L,L holds

( f is Element of S1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds

( f is Element of S2 iff f is directed-sups-preserving ) ) implies S1 = S2 )

assume that

A6: for f being closure Function of L,L holds

( f is Element of S1 iff f is directed-sups-preserving ) and

A7: for f being closure Function of L,L holds

( f is Element of S2 iff f is directed-sups-preserving ) ; :: thesis: S1 = S2

hence S1 = S2 ; :: thesis: verum

let S1, S2 be non empty strict full SubRelStr of ClOpers L; :: thesis: ( ( for f being closure Function of L,L holds

( f is Element of S1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds

( f is Element of S2 iff f is directed-sups-preserving ) ) implies S1 = S2 )

assume that

A6: for f being closure Function of L,L holds

( f is Element of S1 iff f is directed-sups-preserving ) and

A7: for f being closure Function of L,L holds

( f is Element of S2 iff f is directed-sups-preserving ) ; :: thesis: S1 = S2

A8: now :: thesis: for f being object holds

( f is Element of S2 iff S_{1}[f] )

( f is Element of S2 iff S

let f be object ; :: thesis: ( f is Element of S2 iff S_{1}[f] )

( f is Element of S2 implies f is Element of (ClOpers L) ) by YELLOW_0:58;

then ( f is Element of S2 implies f is closure Function of L,L ) by Th10;

hence ( f is Element of S2 iff S_{1}[f] )
by A7; :: thesis: verum

end;( f is Element of S2 implies f is Element of (ClOpers L) ) by YELLOW_0:58;

then ( f is Element of S2 implies f is closure Function of L,L ) by Th10;

hence ( f is Element of S2 iff S

A9: now :: thesis: for f being object holds

( f is Element of S1 iff S_{1}[f] )

RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #)
from WAYBEL10:sch 3(A9, A8);( f is Element of S1 iff S

let f be object ; :: thesis: ( f is Element of S1 iff S_{1}[f] )

( f is Element of S1 implies f is Element of (ClOpers L) ) by YELLOW_0:58;

then ( f is Element of S1 implies f is closure Function of L,L ) by Th10;

hence ( f is Element of S1 iff S_{1}[f] )
by A6; :: thesis: verum

end;( f is Element of S1 implies f is Element of (ClOpers L) ) by YELLOW_0:58;

then ( f is Element of S1 implies f is closure Function of L,L ) by Th10;

hence ( f is Element of S1 iff S

hence S1 = S2 ; :: thesis: verum