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