let SAS be Semi_Affine_Space; for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds
not p,q // p,c
let a, b, c, p, q be Element of SAS; ( not a,b // a,c & p <> q & p,q // p,a & p,q // p,b implies not p,q // p,c )
assume that
A1:
not a,b // a,c
and
A2:
p <> q
; ( not p,q // p,a or not p,q // p,b or not p,q // p,c )
now ( a <> p & p,q // p,a & p,q // p,b implies not p,q // p,c )assume that A3:
a <> p
and A4:
p,
q // p,
a
and A5:
p,
q // p,
b
and A6:
p,
q // p,
c
;
contradiction
p,
a // p,
c
by A2, A4, A6, Def1;
then A7:
a,
p // a,
c
by Def1;
p,
a // p,
b
by A2, A4, A5, Def1;
then
a,
p // a,
b
by Def1;
hence
contradiction
by A1, A3, A7, Def1;
verum end;
hence
( not p,q // p,a or not p,q // p,b or not p,q // p,c )
by A1, A2, Def1; verum