let AS be AffinSpace; 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; 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; ( 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
; contradiction
A4:
b,a // A
by A1, Th33;
A is being_line
by A1;
hence
contradiction
by A2, A3, A4, Th22; verum