let POS be OrtAfSp; :: thesis: for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
let K be Subset of POS; :: thesis: for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
let a, b be Element of POS; :: thesis: ( a in K & b in K & a,b _|_ K implies a = b )
assume that
A1: a in K and
A2: b in K and
A3: a,b _|_ K ; :: thesis: a = b
consider p, q being Element of POS such that
A4: p <> q and
A5: K = Line (p,q) and
A6: a,b _|_ p,q by A3;
reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
set K9 = Line (p9,q9);
b9 in Line (p9,q9) by A2, A5, Th41;
then A7: LIN p9,q9,b9 by AFF_1:def 2;
a9 in Line (p9,q9) by A1, A5, Th41;
then LIN p9,q9,a9 by AFF_1:def 2;
then p9,q9 // a9,b9 by A7, AFF_1:10;
then A8: p,q // a,b by Th36;
p,q _|_ a,b by A6, Def7;
then a,b _|_ a,b by A4, A8, Def7;
hence a = b by Def7; :: thesis: verum