let AS be AffinSpace; :: thesis: for a, b being Element of
for A being Subset of st a,b // A & not a in A holds
not b in A
let a, b be Element of ; :: thesis: for A being Subset of st a,b // A & not a in A holds
not b in A
let A be Subset of ; :: thesis: ( a,b // A & not a in A implies not b in A )
assume that
A1: a,b // A and
A2: not a in A and
A3: b in A ; :: thesis: contradiction
A4: b,a // A by A1, Th48;
A is being_line by A1, Th40;
hence contradiction by A2, A3, A4, Th37; :: thesis: verum