let AS be AffinSpace; 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; 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; ( 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
; d in A
now ( 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
;
d in Athen
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;
verum end;
hence
d in A
by A3; verum