let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies plane p1,p2,p3 = REAL 2 )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; :: thesis: plane p1,p2,p3 = REAL 2
the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:25;
hence plane p1,p2,p3 c= REAL 2 ; :: according to XBOOLE_0:def 10 :: thesis: REAL 2 c= plane p1,p2,p3
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL 2 or x in plane p1,p2,p3 )
assume x in REAL 2 ; :: thesis: x in plane p1,p2,p3
then reconsider p0 = x as Point of (TOP-REAL 2) by EUCLID:25;
set q2 = p2 - p1;
set q3 = p3 - p1;
set p = p0 - p1;
A2: p3 - p1 <> 0. (TOP-REAL 2) by A1, Th59;

now

per cases ( (p3 - p1) `1 <> 0 or (p3 - p1) `2 <> 0 ) by A2, EUCLID:57, EUCLID:58;

case A3: (p3 - p1) `1 <> 0 ; :: thesis: x in plane p1,p2,p3

A4: now

assume (((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )) = 0 ; :: thesis: contradiction
then (p2 - p1) `2 = (((p2 - p1) `1 ) * ((p3 - p1) `2 )) / ((p3 - p1) `1 ) by A3, XCMPLX_1:90;
then p2 - p1 = |[((p2 - p1) `1 ),((((p2 - p1) `1 ) * ((p3 - p1) `2 )) / ((p3 - p1) `1 ))]| by EUCLID:57
.= |[(((p2 - p1) `1 ) * 1),((((p2 - p1) `1 ) * ((p3 - p1) `2 )) * (((p3 - p1) `1 ) " ))]| by XCMPLX_0:def 9
.= |[(((p2 - p1) `1 ) * 1),(((p2 - p1) `1 ) * (((p3 - p1) `2 ) * (((p3 - p1) `1 ) " )))]|
.= ((p2 - p1) `1 ) * |[1,(((p3 - p1) `2 ) * (((p3 - p1) `1 ) " ))]| by EUCLID:62
.= ((p2 - p1) `1 ) * |[((((p3 - p1) `1 ) " ) * ((p3 - p1) `1 )),((((p3 - p1) `1 ) " ) * ((p3 - p1) `2 ))]| by A3, XCMPLX_0:def 7
.= ((p2 - p1) `1 ) * ((((p3 - p1) `1 ) " ) * |[((p3 - p1) `1 ),((p3 - p1) `2 )]|) by EUCLID:62
.= ((p2 - p1) `1 ) * ((((p3 - p1) `1 ) " ) * (p3 - p1)) by EUCLID:57
.= (((p2 - p1) `1 ) * (((p3 - p1) `1 ) " )) * (p3 - p1) by EUCLID:34 ;
then (p2 - p1) + (- ((((p2 - p1) `1 ) * (((p3 - p1) `1 ) " )) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:40;
then (1 * (p2 - p1)) + (- ((((p2 - p1) `1 ) * (((p3 - p1) `1 ) " )) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:33;
then (1 * (p2 - p1)) + ((- (((p2 - p1) `1 ) * (((p3 - p1) `1 ) " ))) * (p3 - p1)) = 0. (TOP-REAL 2) by EUCLID:44;
hence contradiction by A1, Def10; :: thesis: verum

end;

set a = ((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )));
set b = (((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 );
A5: ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * ((p3 - p1) `1 )) = ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )) + (((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) by A3, XCMPLX_1:88
.= (p0 - p1) `1 ;
A6: ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 )) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) = ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 )) + (((((p0 - p1) `1 ) / ((p3 - p1) `1 )) - (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )) / ((p3 - p1) `1 ))) * ((p3 - p1) `2 )) by XCMPLX_1:121
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 )) - ((((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )) / ((p3 - p1) `1 )) * ((p3 - p1) `2 ))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 ))
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 )) - ((((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )) * (((p3 - p1) `1 ) " )) * ((p3 - p1) `2 ))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by XCMPLX_0:def 9
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (((p2 - p1) `2 ) - ((((p2 - p1) `1 ) * (((p3 - p1) `1 ) " )) * ((p3 - p1) `2 )))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 ))
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (((p2 - p1) `2 ) - ((((p2 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by XCMPLX_0:def 9
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (((((p2 - p1) `2 ) / ((p3 - p1) `1 )) * ((p3 - p1) `1 )) - ((((p2 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by A3, XCMPLX_1:88
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (((((p3 - p1) `1 ) / ((p3 - p1) `1 )) * ((p2 - p1) `2 )) - ((((p2 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by XCMPLX_1:76
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (((((p3 - p1) `1 ) * (((p3 - p1) `1 ) " )) * ((p2 - p1) `2 )) - ((((p2 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by XCMPLX_0:def 9
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((((p2 - p1) `2 ) * (((p3 - p1) `1 ) * (((p3 - p1) `1 ) " ))) - (((((p3 - p1) `1 ) " ) * ((p2 - p1) `1 )) * ((p3 - p1) `2 )))) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by XCMPLX_0:def 9
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (((p3 - p1) `1 ) " )) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 ))
.= (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) * (((p3 - p1) `1 ) " )) + ((((p0 - p1) `1 ) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )) by A4, XCMPLX_1:88
.= (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) * (((p3 - p1) `1 ) " )) + (((((p3 - p1) `1 ) " ) * ((p0 - p1) `1 )) * ((p3 - p1) `2 )) by XCMPLX_0:def 9
.= (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) + (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) * (((p3 - p1) `1 ) " )
.= (((p0 - p1) `2 ) * ((p3 - p1) `1 )) / ((p3 - p1) `1 ) by XCMPLX_0:def 9
.= (p0 - p1) `2 by A3, XCMPLX_1:90 ;
A7: ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (p2 - p1)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * (p3 - p1)) = (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p1)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * (p3 - p1)) by EUCLID:53
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2) + (- ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p1))) + ((((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) - (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p1)) by EUCLID:53
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2) + (- ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p1))) + ((((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) + ((- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 ))) * p1)) by EUCLID:44
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2) + ((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) * p1)) + (((- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 ))) * p1) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3)) by EUCLID:44
.= ((((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2) + ((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) * p1)) + ((- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 ))) * p1)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:30
.= (((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2) + (((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) * p1) + ((- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 ))) * p1))) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:30
.= ((((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )))) * p1) + ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:37 ;
((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * (p2 - p1)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * (p3 - p1)) = ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * |[((p2 - p1) `1 ),((p2 - p1) `2 )]|) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * (p3 - p1)) by EUCLID:57
.= ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * |[((p2 - p1) `1 ),((p2 - p1) `2 )]|) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * |[((p3 - p1) `1 ),((p3 - p1) `2 )]|) by EUCLID:57
.= |[((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )),((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 ))]| + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * |[((p3 - p1) `1 ),((p3 - p1) `2 )]|) by EUCLID:62
.= |[((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )),((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 ))]| + |[(((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * ((p3 - p1) `1 )),(((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * ((p3 - p1) `2 ))]| by EUCLID:62
.= |[(((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 )) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * ((p3 - p1) `1 ))),(((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `2 )) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * ((p3 - p1) `2 )))]| by EUCLID:60
.= p0 - p1 by A5, A6, EUCLID:57 ;
then A8: p0 = p1 + (((((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )))) * p1) + ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3)) by A7, EUCLID:52
.= (p1 + ((((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )))) * p1) + ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2))) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:30
.= ((p1 + (((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )))) * p1)) + ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:30
.= (((1 * p1) + (((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )))) * p1)) + ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:33
.= (((1 + ((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 ))))) * p1) + ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * p2)) + (((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) * p3) by EUCLID:37 ;
((1 + ((- (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + (- ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 ))))) + (((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 ))))) + ((((p0 - p1) `1 ) - ((((((p0 - p1) `2 ) * ((p3 - p1) `1 )) - (((p3 - p1) `2 ) * ((p0 - p1) `1 ))) / ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) * ((p2 - p1) `1 ))) / ((p3 - p1) `1 )) = 1 ;
hence x in plane p1,p2,p3 by A8, Th61; :: thesis: verum

end;

case A9: (p3 - p1) `2 <> 0 ; :: thesis: x in plane p1,p2,p3

now

assume (((p2 - p1) `2 ) * ((p3 - p1) `1 )) - (((p2 - p1) `1 ) * ((p3 - p1) `2 )) = 0 ; :: thesis: contradiction
then (p2 - p1) `1 = (((p2 - p1) `2 ) * ((p3 - p1) `1 )) / ((p3 - p1) `2 ) by A9, XCMPLX_1:90;
then p2 - p1 = |[((((p2 - p1) `2 ) * ((p3 - p1) `1 )) / ((p3 - p1) `2 )),((p2 - p1) `2 )]| by EUCLID:57
.= |[((((p2 - p1) `2 ) * ((p3 - p1) `1 )) * (((p3 - p1) `2 ) " )),(((p2 - p1) `2 ) * 1)]| by XCMPLX_0:def 9
.= |[(((p2 - p1) `2 ) * (((p3 - p1) `1 ) * (((p3 - p1) `2 ) " ))),(((p2 - p1) `2 ) * 1)]|
.= ((p2 - p1) `2 ) * |[(((p3 - p1) `1 ) * (((p3 - p1) `2 ) " )),1]| by EUCLID:62
.= ((p2 - p1) `2 ) * |[((((p3 - p1) `2 ) " ) * ((p3 - p1) `1 )),((((p3 - p1) `2 ) " ) * ((p3 - p1) `2 ))]| by A9, XCMPLX_0:def 7
.= ((p2 - p1) `2 ) * ((((p3 - p1) `2 ) " ) * |[((p3 - p1) `1 ),((p3 - p1) `2 )]|) by EUCLID:62
.= ((p2 - p1) `2 ) * ((((p3 - p1) `2 ) " ) * (p3 - p1)) by EUCLID:57
.= (((p2 - p1) `2 ) * (((p3 - p1) `2 ) " )) * (p3 - p1) by EUCLID:34 ;
then (p2 - p1) + (- ((((p2 - p1) `2 ) * (((p3 - p1) `2 ) " )) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:40;
then (1 * (p2 - p1)) + (- ((((p2 - p1) `2 ) * (((p3 - p1) `2 ) " )) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:33;
then (1 * (p2 - p1)) + ((- (((p2 - p1) `2 ) * (((p3 - p1) `2 ) " ))) * (p3 - p1)) = 0. (TOP-REAL 2) by EUCLID:44;
hence contradiction by A1, Def10; :: thesis: verum

end;

then A10: - ((((p2 - p1) `2 ) * ((p3 - p1) `1 )) + (- (((p2 - p1) `1 ) * ((p3 - p1) `2 )))) <> - 0 ;
set a = ((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )));
set b = (((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 );
A11: ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 )) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * ((p3 - p1) `2 )) = ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 )) + (((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) by A9, XCMPLX_1:88
.= (p0 - p1) `2 ;
A12: ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) = ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )) + (((((p0 - p1) `2 ) / ((p3 - p1) `2 )) - (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 )) / ((p3 - p1) `2 ))) * ((p3 - p1) `1 )) by XCMPLX_1:121
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )) - ((((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 )) / ((p3 - p1) `2 )) * ((p3 - p1) `1 ))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 ))
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )) - ((((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 )) * (((p3 - p1) `2 ) " )) * ((p3 - p1) `1 ))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by XCMPLX_0:def 9
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (((p2 - p1) `1 ) - ((((p2 - p1) `2 ) * (((p3 - p1) `2 ) " )) * ((p3 - p1) `1 )))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 ))
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (((p2 - p1) `1 ) - ((((p2 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by XCMPLX_0:def 9
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (((((p2 - p1) `1 ) / ((p3 - p1) `2 )) * ((p3 - p1) `2 )) - ((((p2 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by A9, XCMPLX_1:88
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (((((p3 - p1) `2 ) / ((p3 - p1) `2 )) * ((p2 - p1) `1 )) - ((((p2 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by XCMPLX_1:76
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (((((p3 - p1) `2 ) * (((p3 - p1) `2 ) " )) * ((p2 - p1) `1 )) - ((((p2 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by XCMPLX_0:def 9
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((((p2 - p1) `1 ) * (((p3 - p1) `2 ) * (((p3 - p1) `2 ) " ))) - (((((p3 - p1) `2 ) " ) * ((p2 - p1) `2 )) * ((p3 - p1) `1 )))) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by XCMPLX_0:def 9
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (((p3 - p1) `2 ) " )) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 ))
.= (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) * (((p3 - p1) `2 ) " )) + ((((p0 - p1) `2 ) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )) by A10, XCMPLX_1:88
.= (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) * (((p3 - p1) `2 ) " )) + (((((p3 - p1) `2 ) " ) * ((p0 - p1) `2 )) * ((p3 - p1) `1 )) by XCMPLX_0:def 9
.= (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) + (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) * (((p3 - p1) `2 ) " )
.= (((p0 - p1) `1 ) * ((p3 - p1) `2 )) / ((p3 - p1) `2 ) by XCMPLX_0:def 9
.= (p0 - p1) `1 by A9, XCMPLX_1:90 ;
A13: ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (p2 - p1)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * (p3 - p1)) = (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p1)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * (p3 - p1)) by EUCLID:53
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2) + (- ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p1))) + ((((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) - (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p1)) by EUCLID:53
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2) + (- ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p1))) + ((((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) + ((- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 ))) * p1)) by EUCLID:44
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2) + ((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) * p1)) + (((- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 ))) * p1) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3)) by EUCLID:44
.= ((((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2) + ((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) * p1)) + ((- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 ))) * p1)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:30
.= (((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2) + (((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) * p1) + ((- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 ))) * p1))) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:30
.= ((((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )))) * p1) + ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:37 ;
((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * (p2 - p1)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * (p3 - p1)) = ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * |[((p2 - p1) `1 ),((p2 - p1) `2 )]|) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * (p3 - p1)) by EUCLID:57
.= ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * |[((p2 - p1) `1 ),((p2 - p1) `2 )]|) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * |[((p3 - p1) `1 ),((p3 - p1) `2 )]|) by EUCLID:57
.= |[((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )),((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))]| + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * |[((p3 - p1) `1 ),((p3 - p1) `2 )]|) by EUCLID:62
.= |[((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )),((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))]| + |[(((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * ((p3 - p1) `1 )),(((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * ((p3 - p1) `2 ))]| by EUCLID:62
.= |[(((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `1 )) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * ((p3 - p1) `1 ))),(((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 )) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * ((p3 - p1) `2 )))]| by EUCLID:60
.= p0 - p1 by A11, A12, EUCLID:57 ;
then A14: p0 = p1 + (((((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )))) * p1) + ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3)) by A13, EUCLID:52
.= (p1 + ((((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )))) * p1) + ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2))) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:30
.= ((p1 + (((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )))) * p1)) + ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:30
.= (((1 * p1) + (((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )))) * p1)) + ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:33
.= (((1 + ((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 ))))) * p1) + ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * p2)) + (((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) * p3) by EUCLID:37 ;
((1 + ((- (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + (- ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 ))))) + (((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 ))))) + ((((p0 - p1) `2 ) - ((((((p0 - p1) `1 ) * ((p3 - p1) `2 )) - (((p3 - p1) `1 ) * ((p0 - p1) `2 ))) / ((((p2 - p1) `1 ) * ((p3 - p1) `2 )) - (((p2 - p1) `2 ) * ((p3 - p1) `1 )))) * ((p2 - p1) `2 ))) / ((p3 - p1) `2 )) = 1 ;
hence x in plane p1,p2,p3 by A14, Th61; :: thesis: verum

end;

end;

end;

hence x in plane p1,p2,p3 ; :: thesis: verum