let K be Subset of POS; not K _|_ K
assume
K _|_ K
; 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
by Def15;
reconsider a9 = a, b9 = b as Element of (Af POS) ;
K = Line (a9,b9)
by A2, Th56;
then
( a in K & b in K )
by AFF_1:15;
hence
contradiction
by A1, A3, Th71; verum