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 in A & b in A & c in A & a <> b & a,b // c,d holds
d in A
let a, b, c, d be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A & b in A & c in A & a <> b & a,b // c,d holds
d in A
let A be Subset of AS; :: thesis: ( A is being_line & a in A & b in A & c in A & a <> b & a,b // c,d implies d in A )
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: c in A and
A5: a <> b and
A6: a,b // c,d ; :: thesis: d in A

now

set C = Line c,d;
A7: c in Line c,d by Th26;
A8: d in Line c,d by Th26;
assume A9: c <> d ; :: thesis: d in A
then Line c,d is being_line by Def3;
then A // Line c,d by A1, A2, A3, A5, A6, A9, A7, A8, Th52;
hence d in A by A4, A7, A8, Th59; :: thesis: verum

end;

hence d in A by A4; :: thesis: verum