let M be MidSp; :: thesis: for a, b, c, d being Element of M st [a,b] ## [c,d] holds
a,b @@ c,d
let a, b, c, d be Element of M; :: thesis: ( [a,b] ## [c,d] implies a,b @@ c,d )
assume A1: [a,b] ## [c,d] ; :: thesis: a,b @@ c,d
set p = [a,b];
set q = [c,d];
( [a,b] `1 = a & [a,b] `2 = b & [c,d] `1 = c & [c,d] `2 = d ) by MCART_1:7;
hence a,b @@ c,d by A1, Def6; :: thesis: verum