[:A,B:] = MSAlgebra(# [| the Sorts of A, the Sorts of B|],[[: the Charact of A, the Charact of B:]] #) by PRALG_2:def 15;
hence the Sorts of [:A,B:] is non-empty ; :: according to MSUALG_1:def 8 :: thesis: verum