let MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF be Matrix of 3,F_Real; :: thesis: 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); :: thesis: ( 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*> ; :: thesis: ( 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; :: thesis: verum