defpred S₁[ set , set ] means ex R being RelStr st
( $2 = R & $1 is SubRelStr of R );
defpred S₂[ object ] means $1 is strict SubRelStr of L;
let S1, S2 be non empty strict RelStr ; :: thesis: ( ( 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 S₂[x] ) and
A6: for a, b being Element of S1 holds
( a <= b iff S₁[a,b] ) and
A7: for x being object holds
( x is Element of S2 iff S₂[x] ) and
A8: for a, b being Element of S2 holds
( a <= b iff S₁[a,b] ) ; :: thesis: 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 ; :: thesis: verum