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 & b in K ) and
A2: a,b _|_ K ; :: thesis: a = b
consider p, q being Element of POS such that
A3: ( p <> q & K = Line p,q & a,b _|_ p,q ) by A2, Def14;
reconsider a' = a, b' = b, p' = p, q' = q as Element of (Af POS) ;
set K' = Line p',q';
( a' in Line p',q' & b' in Line p',q' ) by A1, A3, Th56;
then ( LIN p',q',a' & LIN p',q',b' ) by AFF_1:def 2;
then p',q' // a',b' by AFF_1:19;
then A4: p,q // a,b by Th48;
p,q _|_ a,b by A3, Def9;
then a,b _|_ a,b by A3, A4, Def9;
hence a = b by Def9; :: thesis: verum