consider M being MidSp;
consider R being Function of ((n + 2) -tuples_on the carrier of M),the carrier of M;
take ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) ; :: thesis: ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-like
thus ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-like by Lm3; :: thesis: verum