let K, M be Subset of POS; :: thesis: ( K // M implies M // K )
assume K // M ; :: thesis: 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 by Def16;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
a9,b9 // c9,d9 by A2, Th48;
then c9,d9 // a9,b9 by AFF_1:4;
then c,d // a,b by Th48;
hence M // K by A1, Def16; :: thesis: verum