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