let SAS be Semi_Affine_Space; :: thesis: for a, b being Element of st a <> b holds
ex c, d being Element of st parallelogram a,b,c,d
let a, b be Element of ; :: thesis: ( a <> b implies ex c, d being Element of st parallelogram a,b,c,d )
assume a <> b ; :: thesis: ex c, d being Element of st parallelogram a,b,c,d
then consider c being Element of such that
A1: not a,b,c is_collinear by Th41;
ex d being Element of st parallelogram a,b,c,d by A1, Th62;
hence ex c, d being Element of st parallelogram a,b,c,d ; :: thesis: verum