theorem Th20:
for
MABF,
MABE,
MACF,
MBDF,
MCDE,
MACE,
MBDE,
MCDF being
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}| )