let M be MidSp; :: thesis: for a, b, a9, b9, c, c9 being Element of M st a,b @@ a9,b9 & b,c @@ b9,c9 holds
a,c @@ a9,c9
let a, b, a9, b9, c, c9 be Element of M; :: thesis: ( a,b @@ a9,b9 & b,c @@ b9,c9 implies a,c @@ a9,c9 )
assume A1: a,b @@ a9,b9 ; :: thesis: ( not b,c @@ b9,c9 or a,c @@ a9,c9 )
assume A2: b,c @@ b9,c9 ; :: thesis: a,c @@ a9,c9
(b9 @ b) @ (a @ c9) = (a @ b9) @ (b @ c9) by Def4
.= (b @ a9) @ (b @ c9) by A1, Def5
.= (c @ b9) @ (b @ a9) by A2, Def5
.= (b9 @ b) @ (c @ a9) by Def4 ;
hence a @ c9 = c @ a9 by Th18; :: according to MIDSP_1:def 4 :: thesis: verum