defpred S1[ set , set ] means ex R being RelStr st
( $2 = R & $1 is SubRelStr of R );
defpred S2[ object ] means $1 is strict SubRelStr of L;
let S1, S2 be non empty strict RelStr ; ( ( for x being object holds
( x is Element of S1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S1 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) & ( for x being object holds
( x is Element of S2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) implies S1 = S2 )
assume that
A5:
for x being object holds
( x is Element of S1 iff S2[x] )
and
A6:
for a, b being Element of S1 holds
( a <= b iff S1[a,b] )
and
A7:
for x being object holds
( x is Element of S2 iff S2[x] )
and
A8:
for a, b being Element of S2 holds
( a <= b iff S1[a,b] )
; S1 = S2
RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #)
from WAYBEL10:sch 2(A5, A7, A6, A8);
hence
S1 = S2
; verum