let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for A being being_line Subset of AS st 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 being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds
d in A
let A be being_line Subset of AS; :: thesis: ( a in A & b in A & c in A & a <> b & a,b // c,d implies d in A )
assume that
A1: a in A and
A2: b in A and
A3: c in A and
A4: a <> b and
A5: a,b // c,d ; :: thesis: d in A
now :: thesis: ( c <> d implies d in A )
set C = Line (c,d);
A6: c in Line (c,d) by Th14;
A7: d in Line (c,d) by Th14;
assume A8: c <> d ; :: thesis: d in A
then Line (c,d) is being_line ;
then A // Line (c,d) by A1, A2, A4, A5, A8, A6, A7, Th37;
hence d in A by A3, A6, A7, Th44; :: thesis: verum
end;
hence d in A by A3; :: thesis: verum