:: deftheorem Def3 defines commute WAYBEL25:def 3 :
for I being non empty set
for S, T being non empty RelStr
for N being net of T
for i being Element of I st the carrier of T c= the carrier of (S |^ I) holds
for b₆ being strict net of S holds
( b₆ = commute (N,i,S) iff ( RelStr(# the carrier of b₆, the InternalRel of b₆ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₆ = (commute the mapping of N) . i ) );