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