let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for A being Subset of AS st A is being_line & a,b // A & c,d // A holds
a,b // c,d
let a, b, c, d be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a,b // A & c,d // A holds
a,b // c,d
let A be Subset of AS; :: thesis: ( A is being_line & a,b // A & c,d // A implies a,b // c,d )
assume that
A1: A is being_line and
A2: a,b // A and
A3: c,d // A ; :: thesis: a,b // c,d
consider p, q being Element of AS such that
A4: p <> q and
A5: A = Line p,q and
A6: a,b // p,q by A2, Def4;
A7: q in A by A5, Th26;
p in A by A5, Th26;
then c,d // p,q by A1, A3, A4, A7, Th41;
hence a,b // c,d by A4, A6, Th14; :: thesis: verum