let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds
not p,q // p,r
let a, b, c, p, q, r be Element of SAS; :: thesis: ( not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q implies not p,q // p,r )
assume A1:
( not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q )
; :: thesis: not p,q // p,r
now assume
p = r
;
:: thesis: contradictionthen
(
p <> q &
p,
q // a,
b &
p,
q // b,
c )
by A1, Th17;
then
a,
b // b,
c
by Def1;
then
b,
a // b,
c
by Th15;
hence
contradiction
by A1, Th18;
:: thesis: verum end;
hence
not p,q // p,r
by A1, Th29; :: thesis: verum