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