:: deftheorem defines subrelstr YELLOW_0:def 15 :
for L being RelStr
for X being Subset of L
for b₃ being strict full SubRelStr of L holds
( b₃ = subrelstr X iff the carrier of b₃ = X );