let K be Subset of POS; :: thesis: (POS,K,K)
assume (POS,K,K) ; :: thesis: contradiction
then consider a, b being Element of POS such that
A1: a <> b and
A2: K = Line (a,b) and
A3: a,b _|_ K ;
reconsider a9 = a, b9 = b as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
K = Line (a9,b9) by A2, Th41;
then ( a in K & b in K ) by AFF_1:15;
hence contradiction by A1, A3, Th51; :: thesis: verum