let MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF be Matrix of 3,F_Real; for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st 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*> holds
( 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}| )
let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 3); ( 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*> implies ( 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}| ) )
assume that
A1:
MABE = <*p1,p2,p5*>
and
A2:
MACF = <*p1,p3,p6*>
and
A3:
MBDF = <*p2,p4,p6*>
and
A4:
MCDE = <*p3,p4,p5*>
and
A5:
MABF = <*p1,p2,p6*>
and
A6:
MACE = <*p1,p3,p5*>
and
A7:
MBDE = <*p2,p4,p5*>
and
A8:
MCDF = <*p3,p4,p6*>
; ( 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}| )
( 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;
hence
( 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 A1, A2, A3, A4, A5, A6, A7, A8, ANPROJ_8:35; verum