let POS be OrtAfSp; :: thesis: for K being Subset of
for a, b being Element of st a in K & b in K & a,b _|_ K holds
a = b
let K be Subset of ; :: thesis: for a, b being Element of st a in K & b in K & a,b _|_ K holds
a = b
let a, b be Element of ; :: 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 such that
A4: p <> q and
A5: K = Line p,q and
A6: a,b _|_ p,q by A3, Def14;
reconsider a' = a, b' = b, p' = p, q' = q as Element of ;
set K' = Line p',q';
b' in Line p',q' by A2, A5, Th56;
then A7: LIN p',q',b' by AFF_1:def 2;
a' in Line p',q' by A1, A5, Th56;
then LIN p',q',a' by AFF_1:def 2;
then p',q' // a',b' by A7, AFF_1:19;
then A8: p,q // a,b by Th48;
p,q _|_ a,b by A6, Def9;
then a,b _|_ a,b by A4, A8, Def9;
hence a = b by Def9; :: thesis: verum