let AS be AffinSpace; for a, b being Element of AS
for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
let a, b be Element of AS; for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C
let A, C be Subset of AS; ( a in A & b in A & A // C implies a,b // C )
assume that
A1:
a in A
and
A2:
b in A
and
A3:
A // C
; a,b // C
A4:
C is being_line
by A3, Th35;
now a,b // Cconsider p,
q being
Element of
AS such that A5:
p in C
and A6:
q in C
and A7:
p <> q
by A4, Th18;
A8:
C = Line (
p,
q)
by A4, A5, A6, A7, Lm6;
a,
b // p,
q
by A1, A2, A3, A5, A6, Th38;
hence
a,
b // C
by A7, A8;
verum end;
hence
a,b // C
; verum