begin
:: deftheorem Def1 defines LIN AFF_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
Lm1:
for AS being AffinSpace
for x, y, z, t being Element of st x,y // z,t holds
z,t // x,y
theorem Th12:
Lm2:
for AS being AffinSpace
for x, y, z, t being Element of st x,y // z,t holds
y,x // z,t
Lm3:
for AS being AffinSpace
for x, y, z, t being Element of st x,y // z,t holds
x,y // t,z
theorem Th13:
for
AS being
AffinSpace for
x,
y,
z,
t being
Element of 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 Th14:
for
AS being
AffinSpace for
a,
b,
x,
y,
z,
t being
Element of 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 st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z )
theorem Th15:
for
AS being
AffinSpace for
x,
y,
z being
Element of 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 Th16:
theorem Th17:
for
AS being
AffinSpace for
x,
y,
z,
t,
u being
Element of st
x <> y &
LIN x,
y,
z &
LIN x,
y,
t &
LIN x,
y,
u holds
LIN z,
t,
u
theorem Th18:
theorem Th19:
theorem Th20:
for
AS being
AffinSpace for
u,
z,
x,
y,
w being
Element of st
u <> z &
LIN x,
y,
u &
LIN x,
y,
z &
LIN u,
z,
w holds
LIN x,
y,
w
theorem Th21:
theorem
theorem
definition
let AS be
AffinSpace;
let a,
b be
Element of ;
func Line a,
b -> Subset of
means :
Def2:
for
x being
Element of holds
(
x in it iff
LIN a,
b,
x );
existence
ex b1 being Subset of st
for x being Element of holds
( x in b1 iff LIN a,b,x )
uniqueness
for b1, b2 being Subset of st ( for x being Element of holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Line AFF_1:def 2 :
Lm5:
for AS being AffinSpace
for a, b being Element of holds Line a,b c= Line b,a
theorem
canceled;
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem Def3 defines being_line AFF_1:def 3 :
Lm6:
for AS being AffinSpace
for a, b being Element of
for A being Subset of st A is being_line & a in A & b in A & a <> b holds
A = Line a,b
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem Def4 defines // AFF_1:def 4 :
:: deftheorem Def5 defines // AFF_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem
canceled;
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem Th57:
Lm7:
for AS being AffinSpace
for A, C, D being Subset of st A // C & C // D holds
A // D
theorem
theorem Th59:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th68:
for
AS being
AffinSpace for
o,
a,
b,
a',
b' being
Element of st not
LIN o,
a,
b &
LIN o,
a,
a' &
LIN o,
b,
b' &
a' = b' holds
(
a' = o &
b' = o )
theorem Th69:
for
AS being
AffinSpace for
o,
a,
b,
b',
a' being
Element of st not
LIN o,
a,
b &
LIN o,
b,
b' &
a,
b // a',
b' &
a' = o holds
b' = o
theorem
for
AS being
AffinSpace for
o,
a,
b,
a',
b',
x being
Element of st not
LIN o,
a,
b &
LIN o,
a,
a' &
LIN o,
b,
b' &
LIN o,
b,
x &
a,
b // a',
b' &
a,
b // a',
x holds
b' = x
theorem
theorem Th72:
theorem
theorem