let AS be 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 ) )
let a, b, c be Element of AS; ( 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
;
ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A )
A7:
now ( 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 Th14;
assume
a <> c
;
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
;
LIN a,
c,
b
by A2, Th5;
then A10:
b in Line (
a,
c)
by Def2;
a in Line (
a,
c)
by Th14;
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;
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;
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
;
LIN a,b,c
consider p,
q being
Element of
AS such that A19:
p <> q
and A20:
A = Line (
p,
q)
by A15;
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, Th7;
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; verum