let AS be AffinSpace; :: thesis: for A being being_line Subset of AS holds A // A

let A be being_line Subset of AS; :: thesis: A // A

consider a, b being Element of AS such that

A1: a <> b and

A2: A = Line (a,b) by Def3;

a,b // a,b by Th1;

hence A // A by A1, A2, Th36; :: thesis: verum

let A be being_line Subset of AS; :: thesis: A // A

consider a, b being Element of AS such that

A1: a <> b and

A2: A = Line (a,b) by Def3;

a,b // a,b by Th1;

hence A // A by A1, A2, Th36; :: thesis: verum