let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum