let M be MidSp; :: thesis: for a, b, c, a9, b9, c9 being Element of M st a,b @@ a9,b9 & b,c @@ b9,c9 holds

a,c @@ a9,c9

let a, b, c, a9, b9, 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 Def3

.= (b @ a9) @ (b @ c9) by A1

.= (c @ b9) @ (b @ a9) by A2

.= (b9 @ b) @ (c @ a9) by Def3 ;

hence a @ c9 = c @ a9 by Th8; :: according to MIDSP_1:def 4 :: thesis: verum

a,c @@ a9,c9

let a, b, c, a9, b9, 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 Def3

.= (b @ a9) @ (b @ c9) by A1

.= (c @ b9) @ (b @ a9) by A2

.= (b9 @ b) @ (c @ a9) by Def3 ;

hence a @ c9 = c @ a9 by Th8; :: according to MIDSP_1:def 4 :: thesis: verum