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