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