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

A6: now

let x be set ; :: thesis: ( x is Element of S1 iff S₁[x] )
( x is Element of S1 implies x is Element of (Sub L) ) by YELLOW_0:59;
then ( x is Element of S1 implies x is strict SubRelStr of L ) by Def3;
hence ( x is Element of S1 iff S₁[x] ) by A4; :: thesis: verum

end;

A7: now

let x be set ; :: thesis: ( x is Element of S2 iff S₁[x] )
( x is Element of S2 implies x is Element of (Sub L) ) by YELLOW_0:59;
then ( x is Element of S2 implies x is strict SubRelStr of L ) by Def3;
hence ( x is Element of S2 iff S₁[x] ) by A5; :: 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(A6, A7);
hence S1 = S2 ; :: thesis: verum