let M be MidSp; :: thesis: for a, b, c being Element of ex d being Element of st a,b @@ c,d
let a, b, c be Element of ; :: thesis: ex d being Element of st a,b @@ c,d
consider d being Element of such that
A1: d @ a = b @ c by Def4;
a,b @@ c,d by A1, Def5;
hence ex d being Element of st a,b @@ c,d ; :: thesis: verum