begin
Lm1:
for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
z,t // x,y
Lm2:
for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
y,x // z,t
Lm3:
for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
x,y // t,z
theorem Th4:
for
AS being
AffinSpace for
x,
y,
z,
t being
Element of
AS st
x,
y // z,
t holds
(
x,
y // t,
z &
y,
x // z,
t &
y,
x // t,
z &
z,
t // x,
y &
z,
t // y,
x &
t,
z // x,
y &
t,
z // y,
x )
theorem Th5:
for
AS being
AffinSpace for
a,
b,
x,
y,
z,
t being
Element of
AS st
a <> b & ( (
a,
b // x,
y &
a,
b // z,
t ) or (
a,
b // x,
y &
z,
t // a,
b ) or (
x,
y // a,
b &
z,
t // a,
b ) or (
x,
y // a,
b &
a,
b // z,
t ) ) holds
x,
y // z,
t
Lm4:
for AS being AffinSpace
for x, y, z being Element of AS st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z )
theorem Th6:
for
AS being
AffinSpace for
x,
y,
z being
Element of
AS st
LIN x,
y,
z holds
(
LIN x,
z,
y &
LIN y,
x,
z &
LIN y,
z,
x &
LIN z,
x,
y &
LIN z,
y,
x )
theorem Th8:
for
AS being
AffinSpace for
x,
y,
z,
t,
u being
Element of
AS st
x <> y &
LIN x,
y,
z &
LIN x,
y,
t &
LIN x,
y,
u holds
LIN z,
t,
u
theorem Th11:
for
AS being
AffinSpace for
u,
z,
x,
y,
w being
Element of
AS st
u <> z &
LIN x,
y,
u &
LIN x,
y,
z &
LIN u,
z,
w holds
LIN x,
y,
w
Lm5:
for AS being AffinSpace
for a, b being Element of AS holds Line (a,b) c= Line (b,a)
Lm6:
for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds
A = Line (a,b)
Lm7:
for AS being AffinSpace
for A, C, D being Subset of AS st A // C & C // D holds
A // D
theorem Th54:
for
AS being
AffinSpace for
o,
a,
b,
a9,
b9 being
Element of
AS st not
LIN o,
a,
b &
LIN o,
a,
a9 &
LIN o,
b,
b9 &
a9 = b9 holds
(
a9 = o &
b9 = o )
theorem Th55:
for
AS being
AffinSpace for
o,
a,
b,
b9,
a9 being
Element of
AS st not
LIN o,
a,
b &
LIN o,
b,
b9 &
a,
b // a9,
b9 &
a9 = o holds
b9 = o
theorem
for
AS being
AffinSpace for
o,
a,
b,
a9,
b9,
x being
Element of
AS st not
LIN o,
a,
b &
LIN o,
a,
a9 &
LIN o,
b,
b9 &
LIN o,
b,
x &
a,
b // a9,
b9 &
a,
b // a9,
x holds
b9 = x
:: Definition of the Line joining two points
::