let M be MidSp; :: thesis: ex u being Vector of M st
for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 )
consider a being Element of M;
take [a,a] ~ ; :: thesis: for p being Element of [: the carrier of M, the carrier of M:] holds
( p in [a,a] ~ iff p `1 = p `2 )
let p be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p in [a,a] ~ iff p `1 = p `2 )
( [a,a] `1 = a & [a,a] `2 = a ) by MCART_1:7;
then ( p `1 ,p `2 @@ a,a iff p ## [a,a] ) by Def6;
hence ( p in [a,a] ~ iff p `1 = p `2 ) by Th21, Th24, Th41; :: thesis: verum