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] )
set p = [a,b];
set q = [c,d];
A1: ( [a,b] `1 = a & [a,b] `2 = b ) by MCART_1:7;
A2: ( [c,d] `1 = c & [c,d] `2 = d ) by MCART_1:7;
assume a,b @@ c,d ; :: thesis: [a,b] ## [c,d]
hence [a,b] ## [c,d] by A1, A2, Def6; :: thesis: verum