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