let M be MidSp; :: thesis: for a, b, c being Element of M ex d being Element of M st a,b @@ c,d

let a, b, c be Element of M; :: thesis: ex d being Element of M st a,b @@ c,d

consider d being Element of M such that

A1: d @ a = b @ c by Def3;

a,b @@ c,d by A1;

hence ex d being Element of M st a,b @@ c,d ; :: thesis: verum

let a, b, c be Element of M; :: thesis: ex d being Element of M st a,b @@ c,d

consider d being Element of M such that

A1: d @ a = b @ c by Def3;

a,b @@ c,d by A1;

hence ex d being Element of M st a,b @@ c,d ; :: thesis: verum