set FF = the Fanoian Field;
reconsider FdSp = MPS the Fanoian Field as ParSp by Th1;
(1_ the Fanoian Field) + (1_ the Fanoian Field) <> 0. the Fanoian Field by VECTSP_1:def 19;
then A1: for a, b, c, d being Element of FdSp st b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c by Th7;
( not for a, b, c being Element of FdSp holds a,b '||' a,c & ( for a, b, c, p, q, r being Element of FdSp st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r ) ) by Th6, Th8;
then FdSp is FanodesSp-like by A1;
hence ex b₁ being ParSp st
( b₁ is strict & b₁ is FanodesSp-like ) ; :: thesis: verum