let C1, C2 be NatRelStr of n; :: thesis: ( the InternalRel of C1 = [:n,n:] \ (id n) & the InternalRel of C2 = [:n,n:] \ (id n) implies C1 = C2 )
( the carrier of C1 = n & the carrier of C2 = n ) by Def7;
hence ( the InternalRel of C1 = [:n,n:] \ (id n) & the InternalRel of C2 = [:n,n:] \ (id n) implies C1 = C2 ) ; :: thesis: verum