let FdSp be FanodesSp; :: thesis: for a, b, c, d, x being Element of FdSp holds
( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear )
let a, b, c, d, x be Element of FdSp; :: thesis: ( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear )
assume A1: parallelogram a,b,c,d ; :: thesis: ( not a,b,x is_collinear or not c,d,x is_collinear )
then A2: c <> d by Th34;
( not a,b,c is_collinear & a,b '||' c,d ) by A1, Def3;
hence ( not a,b,x is_collinear or not c,d,x is_collinear ) by A2, Th23; :: thesis: verum