let K, M be Subset of POS; :: thesis: ( (POS,K,M) implies (POS,M,K) )
assume K // M ; :: thesis: (POS,M,K)
then consider a, b, c, d being Element of POS such that
A1: ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) ) and
A2: a,b // c,d ;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
a9,b9 // c9,d9 by A2, Th36;
then c9,d9 // a9,b9 by AFF_1:4;
then c,d // a,b by Th36;
hence (POS,M,K) by A1; :: thesis: verum