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