let M be 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:]
let p be Element of [: the carrier of M, the carrier of M:]; { 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:]
set pp = { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } ;
A1:
for x being object st x in { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } holds
x in [: the carrier of M, the carrier of M:]
p in { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p }
;
hence
{ 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:]
by A1, TARSKI:def 3; verum