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 )
( [ the Element of M, the Element of M] `1 = the Element of M & [ the Element of M, the Element of M] `2 = the Element of M ) by MCART_1:7;
then ( p `1 ,p `2 @@ the Element of M, the Element of M iff p ## [ the Element of M, the Element of M] ) by Def6;
hence ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 ) by Th21, Th24, Th41; :: thesis: verum