let AS be 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 )
let a, b be 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 be Subset of AS; ( 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
; 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
;
A4:
d in A
by A2, Th14;
c in A
by A2, Th14;
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; verum