:: deftheorem Def13 defines SubRelStr YELLOW_0:def 13 :
for L, b₂ being RelStr holds
( b₂ is SubRelStr of L iff ( the carrier of b₂ c= the carrier of L & the InternalRel of b₂ c= the InternalRel of L ) );