defpred S1[ 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 S1[f] )
let f be object ; :: thesis: ( f is Element of S2 iff S1[f] )
( f is Element of S2 implies f is Element of () ) 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 S1[f] ) by A7; :: thesis: verum
end;
A9: now :: thesis: for f being object holds
( f is Element of S1 iff S1[f] )
let f be object ; :: thesis: ( f is Element of S1 iff S1[f] )
( f is Element of S1 implies f is Element of () ) 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 S1[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 hence S1 = S2 ; :: thesis: verum