let M be MidSp; :: thesis: for p, q, r being Element of [:the carrier of M,the carrier of M:] st p ## q & p ## r holds
q ## r
let p, q, r be Element of [:the carrier of M,the carrier of M:]; :: thesis: ( p ## q & p ## r implies q ## r )
assume ( p ## q & p ## r ) ; :: thesis: q ## r
then ( p `1 ,p `2 @@ q `1 ,q `2 & p `1 ,p `2 @@ r `1 ,r `2 ) by Def6;
hence q `1 ,q `2 @@ r `1 ,r `2 by Th28; :: according to MIDSP_1:def 6 :: thesis: verum