let M be MidSp; :: thesis: for a, b, c, d being Element of M st [a,b] ~ = [c,d] ~ holds
a @ d = b @ c
let a, b, c, d be Element of M; :: thesis: ( [a,b] ~ = [c,d] ~ implies a @ d = b @ c )
assume [a,b] ~ = [c,d] ~ ; :: thesis: a @ d = b @ c
then a,b @@ c,d by Th32, Th43;
hence a @ d = b @ c by Def5; :: thesis: verum