RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L by Th56;
hence ex b₁ being strict full SubRelStr of L st the carrier of b₁ = X ; :: thesis: verum