let AS be AffinSpace; :: thesis: for a, b being Element of AS

for A being Subset of AS st a,b // A & not a in A holds

not b in A

let a, b be Element of AS; :: thesis: for A being Subset of AS st a,b // A & not a in A holds

not b in A

let A be Subset of AS; :: 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, Th33;

A is being_line by A1;

hence contradiction by A2, A3, A4, Th22; :: thesis: verum

for A being Subset of AS st a,b // A & not a in A holds

not b in A

let a, b be Element of AS; :: thesis: for A being Subset of AS st a,b // A & not a in A holds

not b in A

let A be Subset of AS; :: 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, Th33;

A is being_line by A1;

hence contradiction by A2, A3, A4, Th22; :: thesis: verum