defpred S₁[ object ] means ex y being Element of N st
( y = $1 & i <= y );
let A, B be strict NetStr over L; :: thesis: ( ( for x being object holds
( x in the carrier of A iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of A = the InternalRel of N |_2 the carrier of A & the mapping of A = the mapping of N | the carrier of A & ( for x being object holds
( x in the carrier of B iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of B = the InternalRel of N |_2 the carrier of B & the mapping of B = the mapping of N | the carrier of B implies A = B )
assume that
A2: for x being object holds
( x in the carrier of A iff S₁[x] ) and
A3: ( the InternalRel of A = the InternalRel of N |_2 the carrier of A & the mapping of A = the mapping of N | the carrier of A ) and
A4: for x being object holds
( x in the carrier of B iff S₁[x] ) and
A5: ( the InternalRel of B = the InternalRel of N |_2 the carrier of B & the mapping of B = the mapping of N | the carrier of B ) ; :: thesis: A = B
the carrier of A = the carrier of B from XBOOLE_0:sch 2(A2, A4);
hence A = B by A3, A5; :: thesis: verum