:: deftheorem Def2 defines [: YELLOW_3:def 2 :
for X, Y being RelStr
for b₃ being strict RelStr holds
( b₃ = [:X,Y:] iff ( the carrier of b₃ = [: the carrier of X, the carrier of Y:] & the InternalRel of b₃ = [" the InternalRel of X, the InternalRel of Y"] ) );