let S be OAffinSpace; :: thesis: not for x, y, z being Element of S holds x,y '||' x,z
consider x, y, z, t being Element of S such that
A1:
( not x,y // z,t & not x,y // t,z )
by ANALOAF:def 5;
A2:
( x <> y & z <> t )
by A1, Th7;
now assume A3:
x,
y '||' x,
z
;
:: thesis: not x,y '||' x,tthus
not
x,
y '||' x,
t
:: thesis: verumproof
assume A4:
x,
y '||' x,
t
;
:: thesis: contradiction
then
x,
z '||' x,
t
by A2, A3, Th28;
then
z,
x '||' z,
t
by Th26;
then
x,
z '||' z,
t
by Th27;
then
(
x,
y '||' z,
t or
x = z )
by A3, Th28;
hence
contradiction
by A1, A4, Def4;
:: thesis: verum
end; end;
hence
not for x, y, z being Element of S holds x,y '||' x,z
; :: thesis: verum