:: AFF_1 semantic presentation

begin


definition
let AS be AffinSpace;
let a, b, c be Element of AS;
pred LIN a,b,c means :Def1: :: AFF_1:def 1
a,b // a,c;
end;

:: 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 Th1: :: AFF_1:1
for AS being AffinSpace
for a being Element of AS ex b being Element of AS st a <> b
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS ex b being Element of AS st a <> b
let a be Element of AS; ::_thesis: ex b being Element of AS st a <> b
consider x, y being Element of AS such that
A1: x <> y by DIRAF:40;
 ( a = x implies a <> y ) by A1;
hence  ex b being Element of AS st a <> b ; ::_thesis: verum
end;

theorem Th2: :: AFF_1:2
for AS being AffinSpace
for x, y being Element of AS holds
( x,y // y,x & x,y // x,y )
proof
let AS be AffinSpace; ::_thesis: for x, y being Element of AS holds
( x,y // y,x & x,y // x,y )
let x, y be Element of AS; ::_thesis: ( x,y // y,x & x,y // x,y )
thus  x,y // y,x by DIRAF:40; ::_thesis: x,y // x,y
thus  x,y // x,y by DIRAF:40; ::_thesis: verum
end;

Lm1:  for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
z,t // x,y
proof
let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds
z,t // x,y
let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies z,t // x,y )
assume A1: x,y // z,t ; ::_thesis: z,t // x,y
now__::_thesis:_(_x_<>_y_implies_z,t_//_x,y_)
assume A2: x <> y ; ::_thesis: z,t // x,y
 x,y // x,y by Th2;
hence  z,t // x,y by A1, A2, DIRAF:40; ::_thesis: verum
end;
hence  z,t // x,y by DIRAF:40; ::_thesis: verum
end;

theorem Th3: :: AFF_1:3
for AS being AffinSpace
for x, y, z being Element of AS holds
( x,y // z,z & z,z // x,y )
proof
let AS be AffinSpace; ::_thesis: for x, y, z being Element of AS holds
( x,y // z,z & z,z // x,y )
let x, y, z be Element of AS; ::_thesis: ( x,y // z,z & z,z // x,y )
thus  x,y // z,z by DIRAF:40; ::_thesis: z,z // x,y
hence  z,z // x,y by Lm1; ::_thesis: verum
end;

Lm2:  for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
y,x // z,t
proof
let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds
y,x // z,t
let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies y,x // z,t )
assume A1: x,y // z,t ; ::_thesis: y,x // z,t
 x,y // y,x by Th2;
then  ( y,x // z,t or x = y ) by A1, DIRAF:40;
hence  y,x // z,t by Th3; ::_thesis: verum
end;

Lm3:  for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
x,y // t,z
proof
let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds
x,y // t,z
let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies x,y // t,z )
assume  x,y // z,t ; ::_thesis: x,y // t,z
then  z,t // x,y by Lm1;
then  t,z // x,y by Lm2;
hence  x,y // t,z by Lm1; ::_thesis: verum
end;

theorem Th4: :: AFF_1:4
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies ( 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 ) )
assume A1: x,y // z,t ; ::_thesis: ( 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 )
hence  ( x,y // t,z & y,x // z,t ) by Lm2, Lm3; ::_thesis: ( y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
hence  y,x // t,z by Lm2; ::_thesis: ( z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x )
thus  z,t // x,y by A1, Lm1; ::_thesis: ( z,t // y,x & t,z // x,y & t,z // y,x )
hence  ( z,t // y,x & t,z // x,y ) by Lm2, Lm3; ::_thesis: t,z // y,x
hence  t,z // y,x by Lm3; ::_thesis: verum
end;

theorem Th5: :: AFF_1:5
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, x, y, z, t be Element of AS; ::_thesis: ( 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 ) ) implies x,y // z,t )
assume that
A1: a <> b and
A2: ( ( 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 ) ) ; ::_thesis: x,y // z,t
A3: a,b // z,t by A2, Th4;
 a,b // x,y by A2, Th4;
hence  x,y // z,t by A1, A3, DIRAF:40; ::_thesis: verum
end;

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 )
proof
let AS be AffinSpace; ::_thesis: for x, y, z being Element of AS st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z )
let x, y, z be Element of AS; ::_thesis: ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z ) )
assume  LIN x,y,z ; ::_thesis: ( LIN x,z,y & LIN y,x,z )
then A1: x,y // x,z by Def1;
then A2: y,x // y,z by DIRAF:40;
 x,z // x,y by A1, Th4;
hence  ( LIN x,z,y & LIN y,x,z ) by A2, Def1; ::_thesis: verum
end;

theorem Th6: :: AFF_1:6
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let x, y, z be Element of AS; ::_thesis: ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) )
assume  LIN x,y,z ; ::_thesis: ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
hence  ( LIN x,z,y & LIN y,x,z ) by Lm4; ::_thesis: ( LIN y,z,x & LIN z,x,y & LIN z,y,x )
hence  ( LIN y,z,x & LIN z,x,y ) by Lm4; ::_thesis: LIN z,y,x
hence  LIN z,y,x by Lm4; ::_thesis: verum
end;

theorem Th7: :: AFF_1:7
for AS being AffinSpace
for x, y being Element of AS holds
( LIN x,x,y & LIN x,y,y & LIN x,y,x )
proof
let AS be AffinSpace; ::_thesis: for x, y being Element of AS holds
( LIN x,x,y & LIN x,y,y & LIN x,y,x )
let x, y be Element of AS; ::_thesis: ( LIN x,x,y & LIN x,y,y & LIN x,y,x )
A1: x,y // x,y by Th2;
A2: x,y // x,x by Th3;
 x,x // x,y by Th3;
hence  ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) by A1, A2, Def1; ::_thesis: verum
end;

theorem Th8: :: AFF_1:8
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
proof
let AS be AffinSpace; ::_thesis: 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
let x, y, z, t, u be Element of AS; ::_thesis: ( x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u )
assume that
A1: x <> y and
A2: LIN x,y,z and
A3: LIN x,y,t and
A4: LIN x,y,u ; ::_thesis: LIN z,t,u
A5: now__::_thesis:_(_x_<>_z_implies_LIN_z,t,u_)
A6: x,y // x,z by A2, Def1;
 x,y // x,u by A4, Def1;
then  x,z // x,u by A1, A6, Th5;
then A7: z,x // z,u by DIRAF:40;
 x,y // x,t by A3, Def1;
then  x,z // x,t by A1, A6, Th5;
then A8: z,x // z,t by DIRAF:40;
assume  x <> z ; ::_thesis: LIN z,t,u
then  z,t // z,u by A8, A7, Th5;
hence  LIN z,t,u by Def1; ::_thesis: verum
end;
now__::_thesis:_(_x_=_z_implies_LIN_z,t,u_)
assume A9: x = z ; ::_thesis: LIN z,t,u
then A10: z,y // z,u by A4, Def1;
 z,y // z,t by A3, A9, Def1;
then  z,t // z,u by A1, A9, A10, Th5;
hence  LIN z,t,u by Def1; ::_thesis: verum
end;
hence  LIN z,t,u by A5; ::_thesis: verum
end;

theorem Th9: :: AFF_1:9
for AS being AffinSpace
for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds
LIN x,y,t
proof
let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds
LIN x,y,t
let x, y, z, t be Element of AS; ::_thesis: ( x <> y & LIN x,y,z & x,y // z,t implies LIN x,y,t )
assume that
A1: x <> y and
A2: LIN x,y,z and
A3: x,y // z,t ; ::_thesis: LIN x,y,t
now__::_thesis:_(_z_<>_x_implies_LIN_x,y,t_)
 x,y // x,z by A2, Def1;
then  x,z // z,t by A1, A3, Th5;
then  z,x // z,t by Th4;
then  LIN z,x,t by Def1;
then A4: LIN x,z,t by Th6;
assume A5: z <> x ; ::_thesis: LIN x,y,t
A6: LIN x,z,x by Th7;
 LIN x,z,y by A2, Th6;
hence  LIN x,y,t by A5, A4, A6, Th8; ::_thesis: verum
end;
hence  LIN x,y,t by A3, Def1; ::_thesis: verum
end;

theorem Th10: :: AFF_1:10
for AS being AffinSpace
for x, y, z, t being Element of AS st LIN x,y,z & LIN x,y,t holds
x,y // z,t
proof
let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st LIN x,y,z & LIN x,y,t holds
x,y // z,t
let x, y, z, t be Element of AS; ::_thesis: ( LIN x,y,z & LIN x,y,t implies x,y // z,t )
assume that
A1: LIN x,y,z and
A2: LIN x,y,t ; ::_thesis: x,y // z,t
now__::_thesis:_(_x_<>_y_implies_x,y_//_z,t_)
A3: x,y // x,t by A2, Def1;
A4: x,y // x,z by A1, Def1;
assume  x <> y ; ::_thesis: x,y // z,t
then  x,z // x,t by A4, A3, Th5;
then  z,x // z,t by DIRAF:40;
then  x,z // z,t by Th4;
hence  x,y // z,t by A4, A3, Th5; ::_thesis: verum
end;
hence  x,y // z,t by Th3; ::_thesis: verum
end;

theorem Th11: :: AFF_1:11
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
proof
let AS be AffinSpace; ::_thesis: 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
let u, z, x, y, w be Element of AS; ::_thesis: ( u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w implies LIN x,y,w )
assume that
A1: u <> z and
A2: LIN x,y,u and
A3: LIN x,y,z and
A4: LIN u,z,w ; ::_thesis: LIN x,y,w
now__::_thesis:_(_x_<>_y_implies_LIN_x,y,w_)
assume A5: x <> y ; ::_thesis: LIN x,y,w
 LIN x,y,x by Th7;
then A6: LIN z,u,x by A2, A3, A5, Th8;
 LIN x,y,y by Th7;
then A7: LIN z,u,y by A2, A3, A5, Th8;
 LIN z,u,w by A4, Th6;
hence  LIN x,y,w by A1, A7, A6, Th8; ::_thesis: verum
end;
hence  LIN x,y,w by Th7; ::_thesis: verum
end;

theorem Th12: :: AFF_1:12
for AS being AffinSpace holds
not for x, y, z being Element of AS holds LIN x,y,z
proof
let AS be AffinSpace; ::_thesis: not for x, y, z being Element of AS holds LIN x,y,z
consider x, y, z being Element of AS such that
A1: not x,y // x,z by DIRAF:40;
 not LIN x,y,z by A1, Def1;
hence  not for x, y, z being Element of AS holds LIN x,y,z ; ::_thesis: verum
end;

theorem :: AFF_1:13
for AS being AffinSpace
for x, y being Element of AS st x <> y holds
ex z being Element of AS st not LIN x,y,z
proof
let AS be AffinSpace; ::_thesis: for x, y being Element of AS st x <> y holds
ex z being Element of AS st not LIN x,y,z
let x, y be Element of AS; ::_thesis: ( x <> y implies ex z being Element of AS st not LIN x,y,z )
assume A1: x <> y ; ::_thesis: not for z being Element of AS holds LIN x,y,z
consider a, b, c being Element of AS such that
A2: not LIN a,b,c by Th12;
assume A3: for z being Element of AS holds LIN x,y,z ; ::_thesis: contradiction
then A4: LIN x,y,b ;
A5: LIN x,y,c by A3;
 LIN x,y,a by A3;
hence  contradiction by A1, A2, A4, A5, Th8; ::_thesis: verum
end;

theorem :: AFF_1:14
for AS being AffinSpace
for o, a, b, b9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds
b = b9
proof
let AS be AffinSpace; ::_thesis: for o, a, b, b9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds
b = b9
let o, a, b, b9 be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 implies b = b9 )
assume that
A1: not LIN o,a,b and
A2: LIN o,b,b9 and
A3: a,b // a,b9 ; ::_thesis: b = b9
 LIN a,b,b9 by A3, Def1;
then A4: LIN b,b9,a by Th6;
A5: LIN b,b9,b by Th7;
assume A6: b <> b9 ; ::_thesis: contradiction
 LIN b,b9,o by A2, Th6;
hence  contradiction by A1, A6, A4, A5, Th8; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let a, b be Element of AS;
func Line (a,b) ->  Subset of AS means :Def2: :: AFF_1:def 2
 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 )
proof
defpred S1[ set ] means  for y being Element of AS st y = $1 holds
LIN a,b,y;
consider X being Subset of AS such that
A1: for x being set holds
( x in X iff ( x in the carrier of AS & S1[x] ) ) from SUBSET_1:sch_1();
take  X ; ::_thesis: for x being Element of AS holds
( x in X iff LIN a,b,x )
let x be Element of AS; ::_thesis: ( x in X iff LIN a,b,x )
thus  ( x in X implies LIN a,b,x ) by A1; ::_thesis: ( LIN a,b,x implies x in X )
assume  LIN a,b,x ; ::_thesis: x in X
then  for y being Element of AS st y = x holds
LIN a,b,y ;
hence  x in X by A1; ::_thesis: verum
end;
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
proof
let X1, X2 be Subset of AS; ::_thesis: ( ( for x being Element of AS holds
( x in X1 iff LIN a,b,x ) ) & ( for x being Element of AS holds
( x in X2 iff LIN a,b,x ) ) implies X1 = X2 )
assume that
A2: for x being Element of AS holds
( x in X1 iff LIN a,b,x ) and
A3: for x being Element of AS holds
( x in X2 iff LIN a,b,x ) ; ::_thesis: X1 = X2
 for x being set holds
( x in X1 iff x in X2 )
proof
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
thus  ( x in X1 implies x in X2 ) ::_thesis: ( x in X2 implies x in X1 )
proof
assume A4: x in X1 ; ::_thesis: x in X2
then reconsider x9 = x as Element of AS ;
 LIN a,b,x9 by A2, A4;
hence  x in X2 by A3; ::_thesis: verum
end;
assume A5: x in X2 ; ::_thesis: x in X1
then reconsider x9 = x as Element of AS ;
 LIN a,b,x9 by A3, A5;
hence  x in X1 by A2; ::_thesis: verum
end;
hence  X1 = X2 by TARSKI:1; ::_thesis: verum
end;
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)
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS holds Line (a,b) c= Line (b,a)
let a, b be Element of AS; ::_thesis: Line (a,b) c= Line (b,a)
now__::_thesis:_for_x_being_set_st_x_in_Line_(a,b)_holds_
x_in_Line_(b,a)
let x be set ; ::_thesis: ( x in Line (a,b) implies x in Line (b,a) )
assume A1: x in Line (a,b) ; ::_thesis: x in Line (b,a)
then reconsider x9 = x as Element of AS ;
 LIN a,b,x9 by A1, Def2;
then  LIN b,a,x9 by Th6;
hence  x in Line (b,a) by Def2; ::_thesis: verum
end;
hence  Line (a,b) c= Line (b,a) by TARSKI:def_3; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let a, b be Element of AS;
:: original: Line
redefine func Line (a,b) ->  Subset of AS;
commutativity
 for a, b being Element of AS holds Line (a,b) = Line (b,a)
proof
let a, b be Element of AS; ::_thesis: Line (a,b) = Line (b,a)
A1: Line (b,a) c= Line (a,b) by Lm5;
 Line (a,b) c= Line (b,a) by Lm5;
hence  Line (a,b) = Line (b,a) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

theorem Th15: :: AFF_1:15
for AS being AffinSpace
for a, b being Element of AS holds
( a in Line (a,b) & b in Line (a,b) )
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS holds
( a in Line (a,b) & b in Line (a,b) )
let a, b be Element of AS; ::_thesis: ( a in Line (a,b) & b in Line (a,b) )
A1: LIN a,b,b by Th7;
 LIN a,b,a by Th7;
hence  ( a in Line (a,b) & b in Line (a,b) ) by A1, Def2; ::_thesis: verum
end;

theorem Th16: :: AFF_1:16
for AS being AffinSpace
for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & c <> d holds
Line (c,d) c= Line (a,b)
proof
let AS be AffinSpace; ::_thesis: for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & c <> d holds
Line (c,d) c= Line (a,b)
let c, a, b, d be Element of AS; ::_thesis: ( c in Line (a,b) & d in Line (a,b) & c <> d implies Line (c,d) c= Line (a,b) )
assume that
A1: c in Line (a,b) and
A2: d in Line (a,b) and
A3: c <> d ; ::_thesis: Line (c,d) c= Line (a,b)
A4: LIN a,b,d by A2, Def2;
A5: LIN a,b,c by A1, Def2;
now__::_thesis:_for_x_being_set_st_x_in_Line_(c,d)_holds_
x_in_Line_(a,b)
let x be set ; ::_thesis: ( x in Line (c,d) implies x in Line (a,b) )
assume A6: x in Line (c,d) ; ::_thesis: x in Line (a,b)
then reconsider x9 = x as Element of AS ;
 LIN c,d,x9 by A6, Def2;
then  LIN a,b,x9 by A3, A5, A4, Th11;
hence  x in Line (a,b) by Def2; ::_thesis: verum
end;
hence  Line (c,d) c= Line (a,b) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th17: :: AFF_1:17
for AS being AffinSpace
for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & a <> b holds
Line (a,b) c= Line (c,d)
proof
let AS be AffinSpace; ::_thesis: for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & a <> b holds
Line (a,b) c= Line (c,d)
let c, a, b, d be Element of AS; ::_thesis: ( c in Line (a,b) & d in Line (a,b) & a <> b implies Line (a,b) c= Line (c,d) )
assume that
A1: c in Line (a,b) and
A2: d in Line (a,b) and
A3: a <> b ; ::_thesis: Line (a,b) c= Line (c,d)
A4: LIN a,b,d by A2, Def2;
A5: LIN a,b,c by A1, Def2;
now__::_thesis:_for_x_being_set_st_x_in_Line_(a,b)_holds_
x_in_Line_(c,d)
let x be set ; ::_thesis: ( x in Line (a,b) implies x in Line (c,d) )
assume A6: x in Line (a,b) ; ::_thesis: x in Line (c,d)
then reconsider x9 = x as Element of AS ;
 LIN a,b,x9 by A6, Def2;
then  LIN c,d,x9 by A3, A5, A4, Th8;
hence  x in Line (c,d) by Def2; ::_thesis: verum
end;
hence  Line (a,b) c= Line (c,d) by TARSKI:def_3; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let A be Subset of AS;
attrA is being_line  means :Def3: :: AFF_1:def 3
 ex a, b being Element of AS st
( a <> b & A = Line (a,b) );
end;

:: 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) ) );

registration
let AS be AffinSpace;
cluster being_line for M2(K24( the carrier of AS));
existence
 ex b1 being Subset of AS st b1 is being_line
proof
set a = the Element of AS;
consider b being Element of AS such that
A1: the Element of AS <> b by Th1;
take  Line ( the Element of AS,b) ; ::_thesis: Line ( the Element of AS,b) is being_line
thus  Line ( the Element of AS,b) is being_line by A1, Def3; ::_thesis: verum
end;
end;

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)
proof
let AS be AffinSpace; ::_thesis: 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)
let a, b be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds
A = Line (a,b)
let A be Subset of AS; ::_thesis: ( A is being_line & a in A & b in A & a <> b implies A = Line (a,b) )
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: a <> b ; ::_thesis: A = Line (a,b)
A5: ex p, q being Element of AS st
( p <> q & A = Line (p,q) ) by A1, Def3;
then A6: A c= Line (a,b) by A2, A3, Th17;
 Line (a,b) c= A by A2, A3, A4, A5, Th16;
hence  A = Line (a,b) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th18: :: AFF_1:18
for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds
A = C
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds
A = C
let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds
A = C
let A, C be Subset of AS; ::_thesis: ( A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b implies A = C )
assume that
A1: A is being_line and
A2: C is being_line and
A3: a in A and
A4: b in A and
A5: a in C and
A6: b in C ; ::_thesis: ( a = b or A = C )
assume A7: a <> b ; ::_thesis: A = C
then  A = Line (a,b) by A1, A3, A4, Lm6;
hence  A = C by A2, A5, A6, A7, Lm6; ::_thesis: verum
end;

theorem Th19: :: AFF_1:19
for AS being AffinSpace
for A being Subset of AS st A is being_line holds
ex a, b being Element of AS st
( a in A & b in A & a <> b )
proof
let AS be AffinSpace; ::_thesis: for A being Subset of AS st A is being_line holds
ex a, b being Element of AS st
( a in A & b in A & a <> b )
let A be Subset of AS; ::_thesis: ( A is being_line implies ex a, b being Element of AS st
( a in A & b in A & a <> b ) )
assume  A is being_line ; ::_thesis: ex a, b being Element of AS st
( a in A & b in A & a <> b )
then consider a, b being Element of AS such that
A1: a <> b and
A2: A = Line (a,b) by Def3;
A3: b in A by A2, Th15;
 a in A by A2, Th15;
hence  ex a, b being Element of AS st
( a in A & b in A & a <> b ) by A1, A3; ::_thesis: verum
end;

theorem Th20: :: AFF_1:20
for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is being_line holds
ex b being Element of AS st
( a <> b & b in A )
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS
for A being Subset of AS st A is being_line holds
ex b being Element of AS st
( a <> b & b in A )
let a be Element of AS; ::_thesis: for A being Subset of AS st A is being_line holds
ex b being Element of AS st
( a <> b & b in A )
let A be Subset of AS; ::_thesis: ( A is being_line implies ex b being Element of AS st
( a <> b & b in A ) )
assume  A is being_line ; ::_thesis: ex b being Element of AS st
( a <> b & b in A )
then consider p, q being Element of AS such that
A1: p in A and
A2: q in A and
A3: p <> q by Th19;
 ( a = p implies ( a <> q & q in A ) ) by A2, A3;
hence  ex b being Element of AS st
( a <> b & b in A ) by A1; ::_thesis: verum
end;

theorem Th21: :: AFF_1:21
for AS being AffinSpace
for a, b, c being Element of AS holds
( LIN a,b,c iff ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) )
proof
let AS be AffinSpace; ::_thesis: for a, b, c being Element of AS holds
( LIN a,b,c iff ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) )
let a, b, c be Element of AS; ::_thesis: ( LIN a,b,c iff ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) )
A1: ( LIN a,b,c implies ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) )
proof
assume A2: LIN a,b,c ; ::_thesis: ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A )
A3: now__::_thesis:_(_a_<>_b_implies_ex_A_being_Subset_of_AS_st_
(_A_is_being_line_&_a_in_A_&_b_in_A_&_c_in_A_)_)
set A = Line (a,b);
A4: a in Line (a,b) by Th15;
A5: b in Line (a,b) by Th15;
assume  a <> b ; ::_thesis: ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A )
then A6: Line (a,b) is being_line by Def3;
 c in Line (a,b) by A2, Def2;
hence  ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) by A6, A4, A5; ::_thesis: verum
end;
A7: now__::_thesis:_(_a_<>_c_implies_ex_A_being_Subset_of_AS_st_
(_A_is_being_line_&_a_in_A_&_b_in_A_&_c_in_A_)_)
set A = Line (a,c);
A8: c in Line (a,c) by Th15;
assume  a <> c ; ::_thesis: ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A )
then A9: Line (a,c) is being_line by Def3;
 LIN a,c,b by A2, Th6;
then A10: b in Line (a,c) by Def2;
 a in Line (a,c) by Th15;
hence  ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) by A9, A10, A8; ::_thesis: verum
end;
now__::_thesis:_(_a_=_b_&_a_=_c_implies_ex_A_being_Subset_of_AS_st_
(_A_is_being_line_&_a_in_A_&_b_in_A_&_c_in_A_)_)
consider x being Element of AS such that
A11: a <> x by Th1;
set A = Line (a,x);
A12: a in Line (a,x) by Th15;
assume that
A13: a = b and
A14: a = c ; ::_thesis: ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A )
 Line (a,x) is being_line by A11, Def3;
hence  ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) by A13, A14, A12; ::_thesis: verum
end;
hence  ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) by A3, A7; ::_thesis: verum
end;
 ( ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) implies LIN a,b,c )
proof
given A being Subset of AS such that A15: A is being_line and
A16: a in A and
A17: b in A and
A18: c in A ; ::_thesis: LIN a,b,c
consider p, q being Element of AS such that
A19: p <> q and
A20: A = Line (p,q) by A15, Def3;
A21: LIN p,q,b by A17, A20, Def2;
A22: LIN p,q,c by A18, A20, Def2;
 LIN p,q,a by A16, A20, Def2;
hence  LIN a,b,c by A19, A21, A22, Th8; ::_thesis: verum
end;
hence  ( LIN a,b,c iff ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) ) by A1; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let a, b be Element of AS;
let A be Subset of AS;
preda,b // A means :Def4: :: AFF_1:def 4
 ex c, d being Element of AS st
( c <> d & A = Line (c,d) & a,b // c,d );
end;

:: 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 ) );

definition
let AS be AffinSpace;
let A, C be Subset of AS;
predA // C means :Def5: :: AFF_1:def 5
 ex a, b being Element of AS st
( A = Line (a,b) & a <> b & a,b // C );
end;

:: 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 Th22: :: AFF_1:22
for AS being AffinSpace
for c, a, b, d being Element of AS st c in Line (a,b) & a <> b holds
( d in Line (a,b) iff a,b // c,d )
proof
let AS be AffinSpace; ::_thesis: for c, a, b, d being Element of AS st c in Line (a,b) & a <> b holds
( d in Line (a,b) iff a,b // c,d )
let c, a, b, d be Element of AS; ::_thesis: ( c in Line (a,b) & a <> b implies ( d in Line (a,b) iff a,b // c,d ) )
assume that
A1: c in Line (a,b) and
A2: a <> b ; ::_thesis: ( d in Line (a,b) iff a,b // c,d )
A3: LIN a,b,c by A1, Def2;
thus  ( d in Line (a,b) implies a,b // c,d ) ::_thesis: ( a,b // c,d implies d in Line (a,b) )
proof
assume  d in Line (a,b) ; ::_thesis: a,b // c,d
then  LIN a,b,d by Def2;
hence  a,b // c,d by A3, Th10; ::_thesis: verum
end;
assume  a,b // c,d ; ::_thesis: d in Line (a,b)
then  LIN a,b,d by A2, A3, Th9;
hence  d in Line (a,b) by Def2; ::_thesis: verum
end;

theorem Th23: :: AFF_1:23
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 holds
( b in A iff a,b // A )
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A being Subset of AS st A is being_line & a in A holds
( b in A iff a,b // A )
let a, b be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A holds
( b in A iff a,b // A )
let A be Subset of AS; ::_thesis: ( A is being_line & a in A implies ( b in A iff a,b // A ) )
assume that
A1: A is being_line and
A2: a in A ; ::_thesis: ( b in A iff a,b // A )
consider p, q being Element of AS such that
A3: p <> q and
A4: A = Line (p,q) by A1, Def3;
hereby  ::_thesis: ( a,b // A implies b in A )
assume  b in A ; ::_thesis: a,b // A
then  p,q // a,b by A2, A3, A4, Th22;
then  a,b // p,q by Th4;
hence  a,b // A by A3, A4, Def4; ::_thesis: verum
end;
assume  a,b // A ; ::_thesis: b in A
then consider p, q being Element of AS such that
A5: p <> q and
A6: A = Line (p,q) and
A7: a,b // p,q by Def4;
 p,q // a,b by A7, Th4;
hence  b in A by A2, A5, A6, Th22; ::_thesis: verum
end;

theorem :: AFF_1:24
for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS holds
( a <> b & A = Line (a,b) iff ( A is being_line & a in A & b in A & a <> b ) ) by Def3, Lm6, Th15;

theorem Th25: :: AFF_1:25
for AS being AffinSpace
for a, b, x being Element of AS
for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds
x in A
proof
let AS be AffinSpace; ::_thesis: for a, b, x being Element of AS
for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds
x in A
let a, b, x be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds
x in A
let A be Subset of AS; ::_thesis: ( A is being_line & a in A & b in A & a <> b & LIN a,b,x implies x in A )
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: a <> b and
A5: LIN a,b,x ; ::_thesis: x in A
 A = Line (a,b) by A1, A2, A3, A4, Lm6;
hence  x in A by A5, Def2; ::_thesis: verum
end;

theorem Th26: :: AFF_1:26
for AS being AffinSpace
for A being Subset of AS st ex a, b being Element of AS st a,b // A holds
A is being_line
proof
let AS be AffinSpace; ::_thesis: for A being Subset of AS st ex a, b being Element of AS st a,b // A holds
A is being_line
let A be Subset of AS; ::_thesis: ( ex a, b being Element of AS st a,b // A implies A is being_line )
given a, b being Element of AS such that A1: a,b // A ; ::_thesis: A is being_line
 ex p, q being Element of AS st
( p <> q & A = Line (p,q) & a,b // p,q ) by A1, Def4;
hence  A is being_line by Def3; ::_thesis: verum
end;

theorem Th27: :: AFF_1:27
for AS being AffinSpace
for c, d, a, b being Element of AS
for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds
( a,b // A iff a,b // c,d )
proof
let AS be AffinSpace; ::_thesis: for c, d, a, b being Element of AS
for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds
( a,b // A iff a,b // c,d )
let c, d, a, b be Element of AS; ::_thesis: for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds
( a,b // A iff a,b // c,d )
let A be Subset of AS; ::_thesis: ( c in A & d in A & A is being_line & c <> d implies ( a,b // A iff a,b // c,d ) )
assume that
A1: c in A and
A2: d in A and
A3: A is being_line and
A4: c <> d ; ::_thesis: ( a,b // A iff a,b // c,d )
thus  ( a,b // A implies a,b // c,d ) ::_thesis: ( a,b // c,d implies a,b // A )
proof
assume  a,b // A ; ::_thesis: a,b // c,d
then consider p, q being Element of AS such that
A5: p <> q and
A6: A = Line (p,q) and
A7: a,b // p,q by Def4;
 p,q // c,d by A1, A2, A5, A6, Th22;
hence  a,b // c,d by A5, A7, Th5; ::_thesis: verum
end;
assume A8: a,b // c,d ; ::_thesis: a,b // A
 A = Line (c,d) by A1, A2, A3, A4, Lm6;
hence  a,b // A by A4, A8, Def4; ::_thesis: verum
end;

theorem Th28: :: AFF_1:28
for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st a,b // A holds
ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d )
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A being Subset of AS st a,b // A holds
ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d )
let a, b be Element of AS; ::_thesis: for A being Subset of AS st a,b // A holds
ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d )
let A be Subset of AS; ::_thesis: ( a,b // A implies ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
assume  a,b // A ; ::_thesis: ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d )
then consider c, d being Element of AS such that
A1: c <> d and
A2: A = Line (c,d) and
A3: a,b // c,d by Def4;
A4: d in A by A2, Th15;
 c in A by A2, Th15;
hence  ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) by A1, A3, A4; ::_thesis: verum
end;

theorem Th29: :: AFF_1:29
for AS being AffinSpace
for a, b being Element of AS st a <> b holds
a,b // Line (a,b)
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS st a <> b holds
a,b // Line (a,b)
let a, b be Element of AS; ::_thesis: ( a <> b implies a,b // Line (a,b) )
assume A1: a <> b ; ::_thesis: a,b // Line (a,b)
 a,b // a,b by Th2;
hence  a,b // Line (a,b) by A1, Def4; ::_thesis: verum
end;

theorem Th30: :: AFF_1:30
for AS being AffinSpace
for a, b being Element of AS
for A being being_line Subset of AS holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A being being_line Subset of AS holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
let a, b be Element of AS; ::_thesis: for A being being_line Subset of AS holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
A1: for A being Subset of AS st a,b // A holds
ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) by Th28;
let A be being_line Subset of AS; ::_thesis: ( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )
 ( ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) implies a,b // A )
proof
assume  ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) ; ::_thesis: a,b // A
then consider c, d being Element of AS such that
A2: c <> d and
A3: c in A and
A4: d in A and
A5: a,b // c,d ;
 A = Line (c,d) by A2, A3, A4, Lm6;
hence  a,b // A by A2, A5, Def4; ::_thesis: verum
end;
hence  ( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) ) by A1; ::_thesis: verum
end;

theorem :: AFF_1:31
for AS being AffinSpace
for a, b, c, d being Element of AS
for A being being_line Subset of AS st a,b // A & c,d // A holds
a,b // c,d
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS
for A being being_line Subset of AS st a,b // A & c,d // A holds
a,b // c,d
let a, b, c, d be Element of AS; ::_thesis: for A being being_line Subset of AS st a,b // A & c,d // A holds
a,b // c,d
let A be being_line Subset of AS; ::_thesis: ( a,b // A & c,d // A implies a,b // c,d )
assume that
A1: a,b // A and
A2: c,d // A ; ::_thesis: a,b // c,d
consider p, q being Element of AS such that
A3: p <> q and
A4: A = Line (p,q) and
A5: a,b // p,q by A1, Def4;
A6: q in A by A4, Th15;
 p in A by A4, Th15;
then  c,d // p,q by A2, A3, A6, Th27;
hence  a,b // c,d by A3, A5, Th5; ::_thesis: verum
end;

theorem Th32: :: AFF_1:32
for AS being AffinSpace
for a, b, p, q being Element of AS
for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds
p,q // A
proof
let AS be AffinSpace; ::_thesis: for a, b, p, q being Element of AS
for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds
p,q // A
let a, b, p, q be Element of AS; ::_thesis: for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds
p,q // A
let A be Subset of AS; ::_thesis: ( a,b // A & a,b // p,q & a <> b implies p,q // A )
assume that
A1: a,b // A and
A2: a,b // p,q and
A3: a <> b ; ::_thesis: p,q // A
A4: A is being_line by A1, Th26;
then consider c, d being Element of AS such that
A5: c <> d and
A6: c in A and
A7: d in A and
A8: a,b // c,d by A1, Th30;
 p,q // c,d by A2, A3, A8, Th5;
hence  p,q // A by A4, A5, A6, A7, Th30; ::_thesis: verum
end;

theorem Th33: :: AFF_1:33
for AS being AffinSpace
for a being Element of AS
for A being being_line Subset of AS holds a,a // A
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS
for A being being_line Subset of AS holds a,a // A
let a be Element of AS; ::_thesis: for A being being_line Subset of AS holds a,a // A
let A be being_line Subset of AS; ::_thesis: a,a // A
consider p, q being Element of AS such that
A1: p <> q and
A2: A = Line (p,q) by Def3;
 a,a // p,q by Th3;
hence  a,a // A by A1, A2, Def4; ::_thesis: verum
end;

theorem Th34: :: AFF_1:34
for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st a,b // A holds
b,a // A
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A being Subset of AS st a,b // A holds
b,a // A
let a, b be Element of AS; ::_thesis: for A being Subset of AS st a,b // A holds
b,a // A
let A be Subset of AS; ::_thesis: ( a,b // A implies b,a // A )
assume A1: a,b // A ; ::_thesis: b,a // A
now__::_thesis:_(_a_<>_b_implies_b,a_//_A_)
assume A2: a <> b ; ::_thesis: b,a // A
 a,b // b,a by Th2;
hence  b,a // A by A1, A2, Th32; ::_thesis: verum
end;
hence  b,a // A by A1; ::_thesis: verum
end;

theorem :: AFF_1:35
for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st a,b // A & not a in A holds
not b in A
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A being Subset of AS st a,b // A & not a in A holds
not b in A
let a, b be Element of AS; ::_thesis: for A being Subset of AS st a,b // A & not a in A holds
not b in A
let A be Subset of AS; ::_thesis: ( a,b // A & not a in A implies not b in A )
assume that
A1: a,b // A and
A2: not a in A and
A3: b in A ; ::_thesis: contradiction
A4: b,a // A by A1, Th34;
 A is being_line by A1, Th26;
hence  contradiction by A2, A3, A4, Th23; ::_thesis: verum
end;

theorem Th36: :: AFF_1:36
for AS being AffinSpace
for A, C being Subset of AS st A // C holds
( A is being_line & C is being_line )
proof
let AS be AffinSpace; ::_thesis: for A, C being Subset of AS st A // C holds
( A is being_line & C is being_line )
let A, C be Subset of AS; ::_thesis: ( A // C implies ( A is being_line & C is being_line ) )
assume  A // C ; ::_thesis: ( A is being_line & C is being_line )
then  ex a, b being Element of AS st
( A = Line (a,b) & a <> b & a,b // C ) by Def5;
hence  ( A is being_line & C is being_line ) by Def3, Th26; ::_thesis: verum
end;

theorem Th37: :: AFF_1:37
for AS being AffinSpace
for A, C being Subset of AS holds
( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
proof
let AS be AffinSpace; ::_thesis: for A, C being Subset of AS holds
( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
let A, C be Subset of AS; ::_thesis: ( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
thus  ( A // C implies ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) ::_thesis: ( ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) implies A // C )
proof
assume  A // C ; ::_thesis: ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) )
then consider a, b being Element of AS such that
A1: A = Line (a,b) and
A2: a <> b and
A3: a,b // C by Def5;
 ex c, d being Element of AS st
( c <> d & C = Line (c,d) & a,b // c,d ) by A3, Def4;
hence  ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) by A1, A2; ::_thesis: verum
end;
given a, b, c, d being Element of AS such that A4: a <> b and
A5: c <> d and
A6: a,b // c,d and
A7: A = Line (a,b) and
A8: C = Line (c,d) ; ::_thesis: A // C
 a,b // C by A5, A6, A8, Def4;
hence  A // C by A4, A7, Def5; ::_thesis: verum
end;

theorem Th38: :: AFF_1:38
for AS being AffinSpace
for a, b, c, d being Element of AS
for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds
( A // C iff a,b // c,d )
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS
for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds
( A // C iff a,b // c,d )
let a, b, c, d be Element of AS; ::_thesis: for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds
( A // C iff a,b // c,d )
let A, C be being_line Subset of AS; ::_thesis: ( a in A & b in A & c in C & d in C & a <> b & c <> d implies ( A // C iff a,b // c,d ) )
assume that
A1: a in A and
A2: b in A and
A3: c in C and
A4: d in C and
A5: a <> b and
A6: c <> d ; ::_thesis: ( A // C iff a,b // c,d )
thus  ( A // C implies a,b // c,d ) ::_thesis: ( a,b // c,d implies A // C )
proof
assume  A // C ; ::_thesis: a,b // c,d
then consider p, q, r, s being Element of AS such that
A7: p <> q and
A8: r <> s and
A9: p,q // r,s and
A10: A = Line (p,q) and
A11: C = Line (r,s) by Th37;
 p,q // a,b by A1, A2, A7, A10, Th22;
then A12: a,b // r,s by A7, A9, Th5;
 r,s // c,d by A3, A4, A8, A11, Th22;
hence  a,b // c,d by A8, A12, Th5; ::_thesis: verum
end;
A13: C = Line (c,d) by A3, A4, A6, Lm6;
assume A14: a,b // c,d ; ::_thesis: A // C
 A = Line (a,b) by A1, A2, A5, Lm6;
hence  A // C by A5, A6, A14, A13, Th37; ::_thesis: verum
end;

theorem Th39: :: AFF_1:39
for AS being AffinSpace
for a, b, c, d being Element of AS
for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds
a,b // c,d
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS
for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds
a,b // c,d
let a, b, c, d be Element of AS; ::_thesis: for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds
a,b // c,d
let A, C be Subset of AS; ::_thesis: ( a in A & b in A & c in C & d in C & A // C implies a,b // c,d )
assume that
A1: a in A and
A2: b in A and
A3: c in C and
A4: d in C and
A5: A // C ; ::_thesis: a,b // c,d
now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_a,b_//_c,d_)
A6: C is being_line by A5, Th36;
assume that
A7: a <> b and
A8: c <> d ; ::_thesis: a,b // c,d
 A is being_line by A5, Th36;
hence  a,b // c,d by A1, A2, A3, A4, A5, A7, A8, A6, Th38; ::_thesis: verum
end;
hence  a,b // c,d by Th3; ::_thesis: verum
end;

theorem :: AFF_1:40
for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
let A, C be Subset of AS; ::_thesis: ( a in A & b in A & A // C implies a,b // C )
assume that
A1: a in A and
A2: b in A and
A3: A // C ; ::_thesis: a,b // C
A4: C is being_line by A3, Th36;
now__::_thesis:_a,b_//_C
consider p, q being Element of AS such that
A5: p in C and
A6: q in C and
A7: p <> q by A4, Th19;
A8: C = Line (p,q) by A4, A5, A6, A7, Lm6;
 a,b // p,q by A1, A2, A3, A5, A6, Th39;
hence  a,b // C by A7, A8, Def4; ::_thesis: verum
end;
hence  a,b // C ; ::_thesis: verum
end;

theorem Th41: :: AFF_1:41
for AS being AffinSpace
for A being being_line Subset of AS holds A // A
proof
let AS be AffinSpace; ::_thesis: for A being being_line Subset of AS holds A // A
let A be being_line Subset of AS; ::_thesis: A // A
consider a, b being Element of AS such that
A1: a <> b and
A2: A = Line (a,b) by Def3;
 a,b // a,b by Th2;
hence  A // A by A1, A2, Th37; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let A, B be being_line Subset of AS;
:: original: //
redefine predA // B;
reflexivity
 for A being being_line Subset of AS holds (AS,b1,b1) by Th41;
end;

theorem Th42: :: AFF_1:42
for AS being AffinSpace
for A, C being Subset of AS st A // C holds
C // A
proof
let AS be AffinSpace; ::_thesis: for A, C being Subset of AS st A // C holds
C // A
let A, C be Subset of AS; ::_thesis: ( A // C implies C // A )
assume  A // C ; ::_thesis: C // A
then consider a, b, c, d being Element of AS such that
A1: a <> b and
A2: c <> d and
A3: a,b // c,d and
A4: A = Line (a,b) and
A5: C = Line (c,d) by Th37;
 c,d // a,b by A3, Th4;
hence  C // A by A1, A2, A4, A5, Th37; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let A, C be Subset of AS;
:: original: //
redefine predA // C;
symmetry
 for A, C being Subset of AS st (AS,b1,b2) holds
(AS,b2,b1) by Th42;
end;

theorem Th43: :: AFF_1:43
for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st a,b // A & A // C holds
a,b // C
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A, C being Subset of AS st a,b // A & A // C holds
a,b // C
let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st a,b // A & A // C holds
a,b // C
let A, C be Subset of AS; ::_thesis: ( a,b // A & A // C implies a,b // C )
assume that
A1: a,b // A and
A2: A // C ; ::_thesis: a,b // C
consider p, q, c, d being Element of AS such that
A3: p <> q and
A4: c <> d and
A5: p,q // c,d and
A6: A = Line (p,q) and
A7: C = Line (c,d) by A2, Th37;
A8: q in A by A6, Th15;
A9: A is being_line by A2, Th36;
 p in A by A6, Th15;
then  a,b // p,q by A1, A3, A8, A9, Th27;
then  a,b // c,d by A3, A5, Th5;
hence  a,b // C by A4, A7, Def4; ::_thesis: verum
end;

Lm7:  for AS being AffinSpace
for A, C, D being Subset of AS st A // C & C // D holds
A // D
proof
let AS be AffinSpace; ::_thesis: for A, C, D being Subset of AS st A // C & C // D holds
A // D
let A, C, D be Subset of AS; ::_thesis: ( A // C & C // D implies A // D )
assume that
A1: A // C and
A2: C // D ; ::_thesis: A // D
consider a, b, c, d being Element of AS such that
A3: a <> b and
A4: c <> d and
A5: a,b // c,d and
A6: A = Line (a,b) and
A7: C = Line (c,d) by A1, Th37;
A8: C is being_line by A2, Th36;
A9: d in C by A7, Th15;
A10: D is being_line by A2, Th36;
then consider p, q being Element of AS such that
A11: p <> q and
A12: D = Line (p,q) by Def3;
A13: p in D by A12, Th15;
A14: q in D by A12, Th15;
 c in C by A7, Th15;
then  c,d // p,q by A2, A4, A8, A10, A11, A13, A14, A9, Th38;
then  a,b // p,q by A4, A5, Th5;
hence  A // D by A3, A6, A11, A12, Th37; ::_thesis: verum
end;

theorem :: AFF_1:44
for AS being AffinSpace
for A, C, D being Subset of AS st ( ( A // C & C // D ) or ( A // C & D // C ) or ( C // A & C // D ) or ( C // A & D // C ) ) holds
A // D by Lm7;

theorem Th45: :: AFF_1:45
for AS being AffinSpace
for p being Element of AS
for A, C being Subset of AS st A // C & p in A & p in C holds
A = C
proof
let AS be AffinSpace; ::_thesis: for p being Element of AS
for A, C being Subset of AS st A // C & p in A & p in C holds
A = C
let p be Element of AS; ::_thesis: for A, C being Subset of AS st A // C & p in A & p in C holds
A = C
let A, C be Subset of AS; ::_thesis: ( A // C & p in A & p in C implies A = C )
assume that
A1: A // C and
A2: p in A and
A3: p in C ; ::_thesis: A = C
A4: for A, C being Subset of AS
for p being Element of AS st A // C & p in A & p in C holds
A c= C
proof
let A, C be Subset of AS; ::_thesis: for p being Element of AS st A // C & p in A & p in C holds
A c= C
let p be Element of AS; ::_thesis: ( A // C & p in A & p in C implies A c= C )
assume that
A5: A // C and
A6: p in A and
A7: p in C ; ::_thesis: A c= C
A8: C is being_line by A5, Th36;
A9: A is being_line by A5, Th36;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_C
let x be set ; ::_thesis: ( x in A implies x in C )
assume A10: x in A ; ::_thesis: x in C
then reconsider x9 = x as Element of AS ;
now__::_thesis:_(_x9_<>_p_implies_x_in_C_)
consider q being Element of AS such that
A11: p <> q and
A12: q in C by A8, Th20;
assume A13: x9 <> p ; ::_thesis: x in C
then  A = Line (p,x9) by A6, A9, A10, Lm6;
then  p,x9 // C by A5, A13, Th29, Th43;
then  p,x9 // p,q by A7, A8, A11, A12, Th27;
then  p,q // p,x9 by Th4;
then A14: LIN p,q,x9 by Def1;
 C = Line (p,q) by A7, A8, A11, A12, Lm6;
hence  x in C by A14, Def2; ::_thesis: verum
end;
hence  x in C by A7; ::_thesis: verum
end;
hence  A c= C by TARSKI:def_3; ::_thesis: verum
end;
then A15: C c= A by A1, A2, A3;
 A c= C by A1, A2, A3, A4;
hence  A = C by A15, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: AFF_1:46
for AS being AffinSpace
for x, a, b being Element of AS
for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds
not LIN x,a,b
proof
let AS be AffinSpace; ::_thesis: for x, a, b being Element of AS
for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds
not LIN x,a,b
let x, a, b be Element of AS; ::_thesis: for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds
not LIN x,a,b
let K be Subset of AS; ::_thesis: ( x in K & not a in K & a,b // K & not a = b implies not LIN x,a,b )
assume that
A1: x in K and
A2: not a in K and
A3: a,b // K ; ::_thesis: ( a = b or not LIN x,a,b )
set A = Line (a,b);
assume that
A4: a <> b and
A5: LIN x,a,b ; ::_thesis: contradiction
 LIN a,b,x by A5, Th6;
then A6: x in Line (a,b) by Def2;
A7: a in Line (a,b) by Th15;
 Line (a,b) // K by A3, A4, Def5;
hence  contradiction by A1, A2, A6, A7, Th45; ::_thesis: verum
end;

theorem :: AFF_1:47
for AS being AffinSpace
for a9, b9, p, a, b being Element of AS
for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds
a9 = b9
proof
let AS be AffinSpace; ::_thesis: for a9, b9, p, a, b being Element of AS
for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds
a9 = b9
let a9, b9, p, a, b be Element of AS; ::_thesis: for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds
a9 = b9
let K be Subset of AS; ::_thesis: ( a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b implies a9 = b9 )
assume that
A1: a9,b9 // K and
A2: LIN p,a,a9 and
A3: LIN p,b,b9 and
A4: p in K and
A5: not a in K and
A6: a = b ; ::_thesis: a9 = b9
set A = Line (p,a);
A7: b9 in Line (p,a) by A3, A6, Def2;
A8: p in Line (p,a) by Th15;
A9: a9 in Line (p,a) by A2, Def2;
assume A10: a9 <> b9 ; ::_thesis: contradiction
 Line (p,a) is being_line by A4, A5, Def3;
then  Line (p,a) = Line (a9,b9) by A9, A7, A10, Lm6;
then  Line (p,a) // K by A1, A10, Def5;
then  Line (p,a) = K by A4, A8, Th45;
hence  contradiction by A5, Th15; ::_thesis: verum
end;

theorem :: AFF_1:48
for AS being AffinSpace
for a, b, c, d being Element of AS
for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds
d in A
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS
for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds
d in A
let a, b, c, d be Element of AS; ::_thesis: for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds
d in A
let A be being_line Subset of AS; ::_thesis: ( a in A & b in A & c in A & a <> b & a,b // c,d implies d in A )
assume that
A1: a in A and
A2: b in A and
A3: c in A and
A4: a <> b and
A5: a,b // c,d ; ::_thesis: d in A
now__::_thesis:_(_c_<>_d_implies_d_in_A_)
set C = Line (c,d);
A6: c in Line (c,d) by Th15;
A7: d in Line (c,d) by Th15;
assume A8: c <> d ; ::_thesis: d in A
then  Line (c,d) is being_line by Def3;
then  A // Line (c,d) by A1, A2, A4, A5, A8, A6, A7, Th38;
hence  d in A by A3, A6, A7, Th45; ::_thesis: verum
end;
hence  d in A by A3; ::_thesis: verum
end;

theorem :: AFF_1:49
for AS being AffinSpace
for a being Element of AS
for A being being_line Subset of AS ex C being Subset of AS st
( a in C & A // C )
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS
for A being being_line Subset of AS ex C being Subset of AS st
( a in C & A // C )
let a be Element of AS; ::_thesis: for A being being_line Subset of AS ex C being Subset of AS st
( a in C & A // C )
let A be being_line Subset of AS; ::_thesis: ex C being Subset of AS st
( a in C & A // C )
consider p, q being Element of AS such that
A1: p <> q and
A2: A = Line (p,q) by Def3;
consider b being Element of AS such that
A3: p,q // a,b and
A4: a <> b by DIRAF:40;
set C = Line (a,b);
A5: a in Line (a,b) by Th15;
 A // Line (a,b) by A1, A2, A3, A4, Th37;
hence  ex C being Subset of AS st
( a in C & A // C ) by A5; ::_thesis: verum
end;

theorem :: AFF_1:50
for AS being AffinSpace
for p being Element of AS
for A, C, D being Subset of AS st A // C & A // D & p in C & p in D holds
C = D by Lm7, Th45;

theorem :: AFF_1:51
for AS being AffinSpace
for a, b, c, d being Element of AS
for A being Subset of AS st A is being_line & a in A & b in A & c in A & d in A holds
a,b // c,d by Th39, Th41;

theorem :: AFF_1:52
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 holds
a,b // A by Th23;

theorem :: AFF_1:53
for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds
A // C
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS
for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds
A // C
let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds
A // C
let A, C be Subset of AS; ::_thesis: ( a,b // A & a,b // C & a <> b implies A // C )
assume that
A1: a,b // A and
A2: a,b // C and
A3: a <> b ; ::_thesis: A // C
A4: C is being_line by A2, Th26;
then consider p, q being Element of AS such that
A5: p <> q and
A6: p in C and
A7: q in C and
A8: a,b // p,q by A2, Th30;
A9: A is being_line by A1, Th26;
then consider c, d being Element of AS such that
A10: c <> d and
A11: c in A and
A12: d in A and
A13: a,b // c,d by A1, Th30;
 c,d // p,q by A3, A13, A8, Th5;
hence  A // C by A9, A4, A10, A11, A12, A5, A6, A7, Th38; ::_thesis: verum
end;

theorem Th54: :: AFF_1:54
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let o, a, b, a9, b9 be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 implies ( a9 = o & b9 = o ) )
assume that
A1: not LIN o,a,b and
A2: LIN o,a,a9 and
A3: LIN o,b,b9 and
A4: a9 = b9 ; ::_thesis: ( a9 = o & b9 = o )
set A = Line (o,a);
set C = Line (o,b);
A5: o in Line (o,a) by Th15;
A6: o <> b by A1, Th7;
then A7: Line (o,b) is being_line by Def3;
A8: o <> a by A1, Th7;
then A9: Line (o,a) is being_line by Def3;
A10: a in Line (o,a) by Th15;
then A11: a9 in Line (o,a) by A2, A8, A9, A5, Th25;
A12: b in Line (o,b) by Th15;
A13: o in Line (o,b) by Th15;
then A14: b9 in Line (o,b) by A3, A6, A7, A12, Th25;
 Line (o,a) <> Line (o,b) by A1, A9, A5, A10, A12, Th21;
hence  ( a9 = o & b9 = o ) by A4, A9, A7, A5, A13, A14, A11, Th18; ::_thesis: verum
end;

theorem Th55: :: AFF_1:55
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
proof
let AS be AffinSpace; ::_thesis: 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
let o, a, b, b9, a9 be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o implies b9 = o )
assume that
A1: not LIN o,a,b and
A2: LIN o,b,b9 and
A3: a,b // a9,b9 and
A4: a9 = o ; ::_thesis: b9 = o
A5: now__::_thesis:_not_a,b_//_a9,b
assume  a,b // a9,b ; ::_thesis: contradiction
then  b,a // b,a9 by Th4;
then  LIN b,a,a9 by Def1;
hence  contradiction by A1, A4, Th6; ::_thesis: verum
end;
 a9,b // a9,b9 by A2, A4, Def1;
hence  b9 = o by A3, A4, A5, Th5; ::_thesis: verum
end;

theorem :: AFF_1:56
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
proof
let AS be AffinSpace; ::_thesis: 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
let o, a, b, a9, b9, x be Element of AS; ::_thesis: ( 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 implies b9 = x )
assume that
A1: not LIN o,a,b and
A2: LIN o,a,a9 and
A3: LIN o,b,b9 and
A4: LIN o,b,x and
A5: a,b // a9,b9 and
A6: a,b // a9,x ; ::_thesis: b9 = x
set A = Line (o,a);
set C = Line (o,b);
set P = Line (a9,b9);
A7: a9 in Line (a9,b9) by Th15;
assume A8: b9 <> x ; ::_thesis: contradiction
A9: a9 <> b9
proof
assume A10: a9 = b9 ; ::_thesis: contradiction
then  a9 = o by A1, A2, A3, Th54;
hence  contradiction by A1, A4, A6, A8, A10, Th55; ::_thesis: verum
end;
then A11: Line (a9,b9) is being_line by Def3;
A12: o <> b by A1, Th7;
then A13: Line (o,b) is being_line by Def3;
A14: b9 in Line (a9,b9) by Th15;
 a <> b by A1, Th7;
then  a9,b9 // a9,x by A5, A6, Th5;
then  LIN a9,b9,x by Def1;
then A15: x in Line (a9,b9) by A9, A11, A7, A14, Th25;
A16: b in Line (o,b) by Th15;
A17: o in Line (o,b) by Th15;
then A18: x in Line (o,b) by A4, A12, A13, A16, Th25;
 b9 in Line (o,b) by A3, A12, A13, A17, A16, Th25;
then A19: a9 in Line (o,b) by A8, A13, A11, A7, A14, A18, A15, Th18;
A20: o <> a by A1, Th7;
then A21: Line (o,a) is being_line by Def3;
A22: a9 <> o
proof
assume A23: a9 = o ; ::_thesis: contradiction
then  b9 = o by A1, A3, A5, Th55;
hence  contradiction by A1, A4, A6, A8, A23, Th55; ::_thesis: verum
end;
A24: o in Line (o,a) by Th15;
A25: a in Line (o,a) by Th15;
then  a9 in Line (o,a) by A2, A20, A21, A24, Th25;
then  b in Line (o,a) by A22, A21, A13, A24, A17, A16, A19, Th18;
hence  contradiction by A1, A21, A24, A25, Th21; ::_thesis: verum
end;

theorem :: AFF_1:57
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) by Lm6;


theorem Th58: :: AFF_1:58
for AP being AffinPlane
for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds
ex x being Element of AP st
( x in A & x in C )
proof
let AP be AffinPlane; ::_thesis: for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds
ex x being Element of AP st
( x in A & x in C )
let A, C be Subset of AP; ::_thesis: ( A is being_line & C is being_line & not A // C implies ex x being Element of AP st
( x in A & x in C ) )
assume that
A1: A is being_line and
A2: C is being_line and
A3: not A // C ; ::_thesis: ex x being Element of AP st
( x in A & x in C )
consider a, b being Element of AP such that
A4: a <> b and
A5: A = Line (a,b) by A1, Def3;
consider c, d being Element of AP such that
A6: c <> d and
A7: C = Line (c,d) by A2, Def3;
 not a,b // c,d by A3, A4, A5, A6, A7, Th37;
then consider x being Element of AP such that
A8: a,b // a,x and
A9: c,d // c,x by DIRAF:46;
 LIN c,d,x by A9, Def1;
then A10: x in C by A7, Def2;
 LIN a,b,x by A8, Def1;
then  x in A by A5, Def2;
hence  ex x being Element of AP st
( x in A & x in C ) by A10; ::_thesis: verum
end;

theorem :: AFF_1:59
for AP being AffinPlane
for a, b being Element of AP
for A being Subset of AP st A is being_line & not a,b // A holds
ex x being Element of AP st
( x in A & LIN a,b,x )
proof
let AP be AffinPlane; ::_thesis: for a, b being Element of AP
for A being Subset of AP st A is being_line & not a,b // A holds
ex x being Element of AP st
( x in A & LIN a,b,x )
let a, b be Element of AP; ::_thesis: for A being Subset of AP st A is being_line & not a,b // A holds
ex x being Element of AP st
( x in A & LIN a,b,x )
let A be Subset of AP; ::_thesis: ( A is being_line & not a,b // A implies ex x being Element of AP st
( x in A & LIN a,b,x ) )
assume that
A1: A is being_line and
A2: not a,b // A ; ::_thesis: ex x being Element of AP st
( x in A & LIN a,b,x )
set C = Line (a,b);
A3: not Line (a,b) // A
proof
A4: b in Line (a,b) by Th15;
assume  Line (a,b) // A ; ::_thesis: contradiction
then consider p, q being Element of AP such that
A5: Line (a,b) = Line (p,q) and
A6: p <> q and
A7: p,q // A by Def5;
 a in Line (a,b) by Th15;
then  p,q // a,b by A5, A6, A4, Th22;
hence  contradiction by A2, A6, A7, Th32; ::_thesis: verum
end;
 a <> b by A1, A2, Th33;
then  Line (a,b) is being_line by Def3;
then consider x being Element of AP such that
A8: x in Line (a,b) and
A9: x in A by A1, A3, Th58;
 LIN a,b,x by A8, Def2;
hence  ex x being Element of AP st
( x in A & LIN a,b,x ) by A9; ::_thesis: verum
end;

theorem :: AFF_1:60
for AP being AffinPlane
for a, b, c, d being Element of AP st not a,b // c,d holds
ex p being Element of AP st
( LIN a,b,p & LIN c,d,p )
proof
let AP be AffinPlane; ::_thesis: for a, b, c, d being Element of AP st not a,b // c,d holds
ex p being Element of AP st
( LIN a,b,p & LIN c,d,p )
let a, b, c, d be Element of AP; ::_thesis: ( not a,b // c,d implies ex p being Element of AP st
( LIN a,b,p & LIN c,d,p ) )
assume  not a,b // c,d ; ::_thesis: ex p being Element of AP st
( LIN a,b,p & LIN c,d,p )
then consider p being Element of AP such that
A1: a,b // a,p and
A2: c,d // c,p by DIRAF:46;
A3: LIN c,d,p by A2, Def1;
 LIN a,b,p by A1, Def1;
hence  ex p being Element of AP st
( LIN a,b,p & LIN c,d,p ) by A3; ::_thesis: verum
end;