let POS be OrtAfSp; 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; 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; ( 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
; 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; verum