let e1, e2, e3, f1, f2, f3 be Element of F_Real; :: thesis: for r1, r2 being Real
for p1, p2, p3, p4, p5, p6, p7, p8, p9 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 holds
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
let r1, r2 be Real; :: thesis: for p1, p2, p3, p4, p5, p6, p7, p8, p9 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 holds
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
let p1, p2, p3, p4, p5, p6, p7, p8, p9 be Point of (TOP-REAL 3); :: thesis: ( p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 implies |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}| )
assume that
A1: p1 = <*1,0,0*> and
A2: p2 = <*0,1,0*> and
A3: p3 = <*0,0,1*> and
A4: p4 = <*1,1,1*> and
A5: p5 = <*e1,e2,e3*> and
A6: p6 = <*f1,f2,f3*> and
A7: |{p1,p2,p5}| <> 0 and
A8: |{p1,p3,p6}| <> 0 and
A9: |{p2,p4,p6}| <> 0 and
A10: |{p3,p4,p5}| <> 0 and
A11: |{p1,p2,p6}| <> 0 and
A12: |{p1,p3,p5}| <> 0 and
A13: |{p2,p4,p5}| <> 0 and
A14: |{p3,p4,p6}| <> 0 and
A15: |{p1,p5,p7}| <> 0 and
A16: |{p2,p5,p9}| <> 0 and
A17: |{p5,p9,p7}| <> 0 and
A18: |{p3,p6,p8}| <> 0 and
A19: |{p2,p6,p8}| <> 0 and
A20: |{p2,p9,p7}| <> 0 and
A21: |{p2,p4,p7}| <> 0 and
A22: |{p2,p8,p7}| <> 0 and
A23: |{p3,p5,p8}| <> 0 and
A24: |{p5,p8,p7}| <> 0 and
A25: ( r1 <> 0 or r2 <> 0 ) and
A26: qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 and
A27: qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 and
A28: |{p1,p5,p9}| = 0 and
A29: |{p1,p6,p8}| = 0 and
A30: |{p2,p4,p9}| = 0 and
A31: |{p2,p6,p7}| = 0 and
A32: |{p3,p4,p8}| = 0 and
A33: |{p3,p5,p7}| = 0 ; :: thesis: |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
reconsider r125 = |{p1,p2,p5}|, r136 = |{p1,p3,p6}|, r246 = |{p2,p4,p6}|, r345 = |{p3,p4,p5}|, r126 = |{p1,p2,p6}|, r135 = |{p1,p3,p5}|, r245 = |{p2,p4,p5}|, r346 = |{p3,p4,p6}|, r157 = |{p1,p5,p7}|, r259 = |{p2,p5,p9}|, r597 = |{p5,p9,p7}|, r368 = |{p3,p6,p8}|, r268 = |{p2,p6,p8}|, r297 = |{p2,p9,p7}|, r247 = |{p2,p4,p7}|, r287 = |{p2,p8,p7}|, r358 = |{p3,p5,p8}|, r587 = |{p5,p8,p7}| as non zero Real by A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A24;
( p1 = <*(p1 `1),(p1 `2),(p1 `3)*> & p2 = <*(p2 `1),(p2 `2),(p2 `3)*> & p3 = <*(p3 `1),(p3 `2),(p3 `3)*> & p4 = <*(p4 `1),(p4 `2),(p4 `3)*> & p5 = <*(p5 `1),(p5 `2),(p5 `3)*> & p6 = <*(p6 `1),(p6 `2),(p6 `3)*> ) by EUCLID_5:3;
then reconsider MABE = <*p1,p2,p5*>, MACF = <*p1,p3,p6*>, MBDF = <*p2,p4,p6*>, MCDE = <*p3,p4,p5*>, MABF = <*p1,p2,p6*>, MACE = <*p1,p3,p5*>, MBDE = <*p2,p4,p5*>, MCDF = <*p3,p4,p6*> as Matrix of 3,F_Real by ANPROJ_8:19;
( p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & MABE = <*p1,p2,p5*> & MACF = <*p1,p3,p6*> & MBDF = <*p2,p4,p6*> & MCDE = <*p3,p4,p5*> & MABF = <*p1,p2,p6*> & MACE = <*p1,p3,p5*> & MBDE = <*p2,p4,p5*> & MCDF = <*p3,p4,p6*> ) by A1, A2, A3, A4, A5, A6;
then A34: ( Det MABE = |{p1,p2,p5}| & Det MACF = |{p1,p3,p6}| & Det MBDF = |{p2,p4,p6}| & Det MCDE = |{p3,p4,p5}| & Det MABF = |{p1,p2,p6}| & Det MACE = |{p1,p3,p5}| & Det MBDE = |{p2,p4,p5}| & Det MCDF = |{p3,p4,p6}| ) by Th20;

now :: thesis: ( ((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 & r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) )

( MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> & MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 ) by A1, A2, A3, A4, A5, A6, A25, A26, A27, Th28;
then (((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) by Th19;
hence ((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 by A34; :: thesis: ( r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) )
thus ( r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) ) by A28, A29, A30, A31, A32, A33, Th21, Th22, Th23, Th24, Th25, Th26; :: thesis: verum

end;

hence |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}| by Th27; :: thesis: verum