let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, x being Element of SAS 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 SAS; :: 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 Th54;
( 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, Th44; :: thesis: verum