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 a' = a, b' = b, c' = c, d' = d as Element of (Af POS) ;
a',b' // c',d' by A2, Th48;
then c',d' // a',b' by AFF_1:13;
then c,d // a,b by Th48;
hence M // K by A1, Def16; :: thesis: verum