[#] K = the carrier of V by SIMPLEX0:def 10;
then |.K.| c= [#] K ;
hence BCS K is simplex-join-closed by Th29; :: thesis: verum