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
A4: ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) ) and
A5: a,b _|_ c,d by Th45;
c,d _|_ a,b by A5, Def7;
hence (POS,M,K) by A4, Th45; :: thesis: verum