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 )
set a = the Element of M;
take [ the Element of M, the Element of M] ~ ; :: thesis: for p being Element of [: the carrier of M, the carrier of M:] holds
( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )
let p be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )
( p `1 ,p `2 @@ the Element of M, the Element of M iff p ## [ the Element of M, the Element of M] ) ;
hence ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 ) by Th13, Th26; :: thesis: verum