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 parallelogram a,b,c,d ; :: thesis: ( not a,b,x is_collinear or not c,d,x is_collinear )
then ( not a,b,c is_collinear & a,b // c,d & c <> d ) by Def3, Th54;
hence ( not a,b,x is_collinear or not c,d,x is_collinear ) by Th44; :: thesis: verum