set R = nabla the carrier of M;
let v, v9, w, w9 be Element of M; :: according to ALGSTR_4:def 3 :: thesis: ( v in Class (nabla the carrier of M),v9 & w in Class (nabla the carrier of M),w9 implies v * w in Class (nabla the carrier of M),(v9 * w9) )
assume ( v in Class (nabla the carrier of M),v9 & w in Class (nabla the carrier of M),w9 ) ; :: thesis: v * w in Class (nabla the carrier of M),(v9 * w9)
then A1: not M is empty ;
then Class (nabla the carrier of M),(v9 * w9) = the carrier of M by EQREL_1:34;
hence v * w in Class (nabla the carrier of M),(v9 * w9) by A1, SUBSET_1:def 2; :: thesis: verum