let SAS be Semi_Affine_Space; for o, p, q, r, s being Element of SAS st p,q // r,s holds
p,q // sum (p,r,o), sum (q,s,o)
let o, p, q, r, s be Element of SAS; ( p,q // r,s implies p,q // sum (p,r,o), sum (q,s,o) )
assume A1:
p,q // r,s
; p,q // sum (p,r,o), sum (q,s,o)
now ( p <> q & r <> s implies p,q // sum (p,r,o), sum (q,s,o) )consider t being
Element of
SAS such that A2:
congr o,
q,
r,
t
by Th63;
assume that A3:
p <> q
and A4:
r <> s
;
p,q // sum (p,r,o), sum (q,s,o)
congr o,
q,
s,
sum (
q,
s,
o)
by Def5;
then
congr r,
t,
s,
sum (
q,
s,
o)
by A2, Th65;
then A5:
congr r,
s,
t,
sum (
q,
s,
o)
by Th69;
then A6:
t <> sum (
q,
s,
o)
by A4, Th55;
r,
s // t,
sum (
q,
s,
o)
by A5, Th57;
then A7:
p,
q // t,
sum (
q,
s,
o)
by A1, A4, Th8;
congr o,
p,
r,
sum (
p,
r,
o)
by Def5;
then
congr p,
o,
sum (
p,
r,
o),
r
by Th69;
then
congr p,
q,
sum (
p,
r,
o),
t
by A2, Th70;
then
p,
q // sum (
p,
r,
o),
t
by Th57;
then
p,
q // t,
sum (
p,
r,
o)
by Th6;
then
t,
sum (
q,
s,
o)
// t,
sum (
p,
r,
o)
by A3, A7, Def1;
then
t,
sum (
q,
s,
o)
// sum (
p,
r,
o),
sum (
q,
s,
o)
by Th7;
hence
p,
q // sum (
p,
r,
o),
sum (
q,
s,
o)
by A6, A7, Th8;
verum end;
hence
p,q // sum (p,r,o), sum (q,s,o)
by Th3, Th85; verum