let M be MidSp; :: thesis: for a, b, c, d, x, y being Element of M st x,y @@ a,b & x,y @@ c,d holds

a,b @@ c,d

let a, b, c, d, x, y be Element of M; :: thesis: ( x,y @@ a,b & x,y @@ c,d implies a,b @@ c,d )

assume A1: x,y @@ a,b ; :: thesis: ( not x,y @@ c,d or a,b @@ c,d )

assume A2: x,y @@ c,d ; :: thesis: a,b @@ c,d

(y @ x) @ (a @ d) = (y @ a) @ (x @ d) by Def3

.= (x @ b) @ (x @ d) by A1

.= (x @ b) @ (y @ c) by A2

.= (y @ x) @ (b @ c) by Def3 ;

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

a,b @@ c,d

let a, b, c, d, x, y be Element of M; :: thesis: ( x,y @@ a,b & x,y @@ c,d implies a,b @@ c,d )

assume A1: x,y @@ a,b ; :: thesis: ( not x,y @@ c,d or a,b @@ c,d )

assume A2: x,y @@ c,d ; :: thesis: a,b @@ c,d

(y @ x) @ (a @ d) = (y @ a) @ (x @ d) by Def3

.= (x @ b) @ (x @ d) by A1

.= (x @ b) @ (y @ c) by A2

.= (y @ x) @ (b @ c) by Def3 ;

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