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 ;
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; :: thesis: verum