let K, M be Subset of POS; ( (POS,K,M) implies (POS,M,K) )
assume
K _|_ M
; (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; verum