[: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