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:22;
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 object ; :: 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:22;
set q2 = p2 - p1;
set q3 = p3 - p1;
set p = p0 - p1;
A2: p3 - p1 <> 0. (TOP-REAL 2) by A1, Th50;

now :: thesis: ( ( (p3 - p1) `1 <> 0 & x in plane (p1,p2,p3) ) or ( (p3 - p1) `2 <> 0 & x in plane (p1,p2,p3) ) )

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

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

A4: now :: thesis: not (((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)) = 0

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:89;
then p2 - p1 = |[((p2 - p1) `1),((((p2 - p1) `1) * ((p3 - p1) `2)) / ((p3 - p1) `1))]| by EUCLID:53
.= |[(((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:58
.= ((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:58
.= ((p2 - p1) `1) * ((((p3 - p1) `1) ") * (p3 - p1)) by EUCLID:53
.= (((p2 - p1) `1) * (((p3 - p1) `1) ")) * (p3 - p1) by RLVECT_1:def 7 ;
then (p2 - p1) + (- ((((p2 - p1) `1) * (((p3 - p1) `1) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by RLVECT_1:5;
then (1 * (p2 - p1)) + (- ((((p2 - p1) `1) * (((p3 - p1) `1) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by RLVECT_1:def 8;
then (1 * (p2 - p1)) + ((- (((p2 - p1) `1) * (((p3 - p1) `1) "))) * (p3 - p1)) = 0. (TOP-REAL 2) by RLVECT_1:79;
hence contradiction by A1; :: 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:87
.= (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:120
.= (((((((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:87
.= ((((((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:75
.= ((((((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:87
.= (((((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:89 ;
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 RLVECT_1:34
.= (((((((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 RLVECT_1:34
.= (((((((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 RLVECT_1:79
.= (((((((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 RLVECT_1:79
.= ((((((((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 RLVECT_1:def 3
.= (((((((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 RLVECT_1:def 3
.= ((((- (((((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 RLVECT_1:def 6 ;
((((((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: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 - 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: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 - 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:58
.= |[((((((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:58
.= |[(((((((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:56
.= p0 - p1 by A5, A6, EUCLID:53 ;
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, RLVECT_4: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 RLVECT_1:def 3
.= ((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 RLVECT_1:def 3
.= (((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 RLVECT_1:def 8
.= (((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 RLVECT_1:def 6 ;
((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, Th52; :: thesis: verum

end;

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

now :: thesis: not (((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)) = 0

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:89;
then p2 - p1 = |[((((p2 - p1) `2) * ((p3 - p1) `1)) / ((p3 - p1) `2)),((p2 - p1) `2)]| by EUCLID:53
.= |[((((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:58
.= ((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:58
.= ((p2 - p1) `2) * ((((p3 - p1) `2) ") * (p3 - p1)) by EUCLID:53
.= (((p2 - p1) `2) * (((p3 - p1) `2) ")) * (p3 - p1) by RLVECT_1:def 7 ;
then (p2 - p1) + (- ((((p2 - p1) `2) * (((p3 - p1) `2) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by RLVECT_1:5;
then (1 * (p2 - p1)) + (- ((((p2 - p1) `2) * (((p3 - p1) `2) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by RLVECT_1:def 8;
then (1 * (p2 - p1)) + ((- (((p2 - p1) `2) * (((p3 - p1) `2) "))) * (p3 - p1)) = 0. (TOP-REAL 2) by RLVECT_1:79;
hence contradiction by A1; :: 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:87
.= (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:120
.= (((((((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:87
.= ((((((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:75
.= ((((((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:87
.= (((((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:89 ;
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 RLVECT_1:34
.= (((((((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 RLVECT_1:34
.= (((((((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 RLVECT_1:79
.= (((((((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 RLVECT_1:79
.= ((((((((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 RLVECT_1:def 3
.= (((((((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 RLVECT_1:def 3
.= ((((- (((((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 RLVECT_1:def 6 ;
((((((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: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 - 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: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 - 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:58
.= |[((((((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:58
.= |[(((((((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:56
.= p0 - p1 by A11, A12, EUCLID:53 ;
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, RLVECT_4: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 RLVECT_1:def 3
.= ((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 RLVECT_1:def 3
.= (((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 RLVECT_1:def 8
.= (((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 RLVECT_1:def 6 ;
((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, Th52; :: thesis: verum

end;

end;

end;

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