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