let AS be 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 ) )
let a, b be 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 ) )
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 Th27;
let A be being_line Subset of AS; ( 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 )
;
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;
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; verum