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