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