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