let M be MidSp; :: thesis: for x, y, a, b, c, d being Element of M st x,y @@ a,b & x,y @@ c,d holds
a,b @@ c,d
let x, y, a, b, c, d 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 Def4
.= (x @ b) @ (x @ d) by A1, Def5
.= (x @ b) @ (y @ c) by A2, Def5
.= (y @ x) @ (b @ c) by Def4 ;
hence a @ d = b @ c by Th18; :: according to MIDSP_1:def 4 :: thesis: verum