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