defpred S₁[ set ] means ex y being Element of N st
( y = $1 & i <= y );
let A, B be strict NetStr of L; :: thesis: ( ( for x being set 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 set 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 set 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 and
A4: the mapping of A = the mapping of N | the carrier of A and
A5: for x being set holds
( x in the carrier of B iff S₁[x] ) and
A6: the InternalRel of B = the InternalRel of N |_2 the carrier of B and
A7: 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, A5);
hence A = B by A3, A4, A6, A7; :: thesis: verum