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

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 )

hence
d in A
by A3; :: thesis: verumset 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;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