defpred S₁[ object ] means $1 is strict full infs-inheriting SubRelStr of L;
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 infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds
( R is Element of S2 iff ( R is infs-inheriting & 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 infs-inheriting & R is full ) ) and
A5: for R being strict SubRelStr of L holds
( R is Element of S2 iff ( R is infs-inheriting & R is full ) ) ; :: 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 (Sub L) ) by YELLOW_0:58;
then ( x is Element of S2 implies x is strict SubRelStr of L ) by Def2;
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 (Sub L) ) by YELLOW_0:58;
then ( x is Element of S1 implies x is strict SubRelStr of L ) by Def2;
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