begin
:: deftheorem Def1 defines LIN AFF_1:def 1 :
for AS being AffinSpace
for a, b, c being Element of AS holds
( LIN a,b,c iff a,b // a,c );
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 AS 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 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 Th13:
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 Th14:
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 Th15:
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 Th16:
theorem Th17:
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 Th18:
theorem Th19:
theorem Th20:
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
theorem Th21:
theorem
theorem
definition
let AS be
AffinSpace;
let a,
b be
Element of
AS;
func Line (
a,
b)
-> Subset of
AS means :
Def2:
for
x being
Element of
AS holds
(
x in it iff
LIN a,
b,
x );
existence
ex b1 being Subset of AS st
for x being Element of AS holds
( x in b1 iff LIN a,b,x )
uniqueness
for b1, b2 being Subset of AS st ( for x being Element of AS holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of AS holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Line AFF_1:def 2 :
for AS being AffinSpace
for a, b being Element of AS
for b4 being Subset of AS holds
( b4 = Line (a,b) iff for x being Element of AS holds
( x in b4 iff LIN a,b,x ) );
Lm5:
for AS being AffinSpace
for a, b being Element of AS holds Line (a,b) c= Line (b,a)
theorem
canceled;
theorem
canceled;
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem Def3 defines being_line AFF_1:def 3 :
for AS being AffinSpace
for A being Subset of AS holds
( A is being_line iff ex a, b being Element of AS st
( a <> b & A = Line (a,b) ) );
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)
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem Def4 defines // AFF_1:def 4 :
for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & A = Line (c,d) & a,b // c,d ) );
:: deftheorem Def5 defines // AFF_1:def 5 :
for AS being AffinSpace
for A, C being Subset of AS holds
( A // C iff ex a, b being Element of AS st
( A = Line (a,b) & a <> b & a,b // C ) );
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
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 AS 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,
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 Th69:
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
theorem
theorem Th72:
theorem
theorem