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

for A being Subset of AS st ( a,b // A or b,a // A ) & a in A holds

b in A

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

b in A

let A be Subset of AS; :: thesis: ( ( a,b // A or b,a // A ) & a in A implies b in A )

assume that

A1: ( a,b // A or b,a // A ) and

A2: a in A ; :: thesis: b in A

( a,b // A & A is being_line ) by A1, AFF_1:26, AFF_1:34;

hence b in A by A2, AFF_1:23; :: thesis: verum

for A being Subset of AS st ( a,b // A or b,a // A ) & a in A holds

b in A

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

b in A

let A be Subset of AS; :: thesis: ( ( a,b // A or b,a // A ) & a in A implies b in A )

assume that

A1: ( a,b // A or b,a // A ) and

A2: a in A ; :: thesis: b in A

( a,b // A & A is being_line ) by A1, AFF_1:26, AFF_1:34;

hence b in A by A2, AFF_1:23; :: thesis: verum