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 are_collinear or not c,d,x are_collinear )
let a, b, c, d, x be Element of SAS; :: thesis: ( not parallelogram a,b,c,d or not a,b,x are_collinear or not c,d,x are_collinear )
assume A1: parallelogram a,b,c,d ; :: thesis: ( not a,b,x are_collinear or not c,d,x are_collinear )
then A2: c <> d by Th36;
( not a,b,c are_collinear & a,b // c,d ) by A1;
hence ( not a,b,x are_collinear or not c,d,x are_collinear ) by A2, Th28; :: thesis: verum