defpred S₁[ object ] means $1 is strict closure directed-sups-inheriting System of L;
let S1, S2 be non empty strict full SubRelStr of ClosureSystems L; :: thesis: ( ( for R being strict closure System of L holds
( R is Element of S1 iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds
( R is Element of S2 iff R is directed-sups-inheriting ) ) implies S1 = S2 )
assume that
A4: for R being strict closure System of L holds
( R is Element of S1 iff R is directed-sups-inheriting ) and
A5: for R being strict closure System of L holds
( R is Element of S2 iff R is directed-sups-inheriting ) ; :: thesis: S1 = S2

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

let x be object ; :: thesis: ( x is Element of S2 iff S₁[x] )
( x is Element of S2 implies x is Element of (ClosureSystems L) ) by YELLOW_0:58;
then ( x is Element of S2 implies x is strict closure System of L ) by Th16;
hence ( x is Element of S2 iff S₁[x] ) by A5; :: thesis: verum

end;

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

let x be object ; :: thesis: ( x is Element of S1 iff S₁[x] )
( x is Element of S1 implies x is Element of (ClosureSystems L) ) by YELLOW_0:58;
then ( x is Element of S1 implies x is strict closure System of L ) by Th16;
hence ( x is Element of S1 iff S₁[x] ) by A4; :: 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(A7, A6);
hence S1 = S2 ; :: thesis: verum