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
A2: c <> d and
A3: A = Line (c,d) and
A4: a,b // c,d by Def4;
A5: d in A by A3, Th26;
c in A by A3, Th26;
hence ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) by A2, A4, A5; :: thesis: verum