let M be MidSp; :: thesis: 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:]; :: thesis: { 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 set 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:]

proof

let x be set ; :: thesis: ( x in { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } implies x in [: the carrier of M, the carrier of M:] )
assume x in { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } ; :: thesis: x in [: the carrier of M, the carrier of M:]
then ex q being Element of [: the carrier of M, the carrier of M:] st
( x = q & q ## p ) ;
hence x in [: the carrier of M, the carrier of M:] ; :: thesis: verum

end;

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; :: thesis: verum