ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence for b₁ being set st b₁ = X `2 holds
( b₁ is Function-like & b₁ is Relation-like ) ; :: thesis: verum