ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence for b₁ being Relation st b₁ = X `1 holds
b₁ is A -defined ; :: thesis: verum