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