let M be MidSp; :: thesis: for a, b, c, d, d9 being Element of M st a,b @@ c,d & a,b @@ c,d9 holds
d = d9
let a, b, c, d, d9 be Element of M; :: thesis: ( a,b @@ c,d & a,b @@ c,d9 implies d = d9 )
assume A1: a,b @@ c,d ; :: thesis: ( not a,b @@ c,d9 or d = d9 )
assume A2: a,b @@ c,d9 ; :: thesis: d = d9
a @ d = b @ c by A1, Def5
.= a @ d9 by A2, Def5 ;
hence d = d9 by Th18; :: thesis: verum