defpred S₁[ 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

A8: now :: thesis: for f being object holds
( f is Element of S2 iff S₁[f] )

let f be object ; :: thesis: ( f is Element of S2 iff S₁[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₁[f] ) by A7; :: thesis: verum

end;

A9: now :: thesis: for f being object holds
( f is Element of S1 iff S₁[f] )

let f be object ; :: thesis: ( f is Element of S1 iff S₁[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₁[f] ) by A6; :: thesis: verum

end;

RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch 3(A9, A8);
hence S1 = S2 ; :: thesis: verum