theorem Th25: :: MIDSP_1:25

for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } is non empty Subset of [: the carrier of M, the carrier of M:]