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 Th20, Th28;

hence a @ d = b @ c ; :: thesis: verum

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 Th20, Th28;

hence a @ d = b @ c ; :: thesis: verum