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 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:]

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

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 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:]

proof

p in { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p }
;
let x be object ; :: 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;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

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