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

for A being being_line Subset of AS st a,b // A & c,d // A holds

a,b // c,d

let a, b, c, d be Element of AS; :: thesis: for A being being_line Subset of AS st a,b // A & c,d // A holds

a,b // c,d

let A be being_line Subset of AS; :: thesis: ( a,b // A & c,d // A implies a,b // c,d )

assume that

A1: a,b // A and

A2: c,d // A ; :: thesis: a,b // c,d

consider p, q being Element of AS such that

A3: p <> q and

A4: A = Line (p,q) and

A5: a,b // p,q by A1;

A6: q in A by A4, Th14;

p in A by A4, Th14;

then c,d // p,q by A2, A3, A6, Th26;

hence a,b // c,d by A3, A5, Th4; :: thesis: verum

for A being being_line Subset of AS st a,b // A & c,d // A holds

a,b // c,d

let a, b, c, d be Element of AS; :: thesis: for A being being_line Subset of AS st a,b // A & c,d // A holds

a,b // c,d

let A be being_line Subset of AS; :: thesis: ( a,b // A & c,d // A implies a,b // c,d )

assume that

A1: a,b // A and

A2: c,d // A ; :: thesis: a,b // c,d

consider p, q being Element of AS such that

A3: p <> q and

A4: A = Line (p,q) and

A5: a,b // p,q by A1;

A6: q in A by A4, Th14;

p in A by A4, Th14;

then c,d // p,q by A2, A3, A6, Th26;

hence a,b // c,d by A3, A5, Th4; :: thesis: verum