:: deftheorem Def8 defines CompleteRelStr MYCIELSK:def 8 :
for n being Nat
for b₂ being NatRelStr of n holds
( b₂ = CompleteRelStr n iff the InternalRel of b₂ = [:n,n:] \ (id n) );