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