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