let POS be OrtAfPl; :: thesis: for M, N being Subset of POS st M _|_ N holds
ex p being Element of POS st
( p in M & p in N )
let M, N be Subset of POS; :: thesis: ( M _|_ N implies ex p being Element of POS st
( p in M & p in N ) )
reconsider M9 = M, N9 = N as Subset of (Af POS) ;
assume A1: M _|_ N ; :: thesis: ex p being Element of POS st
( p in M & p in N )
then M is being_line by Th62;
then A2: M9 is being_line by Th58;
N is being_line by A1, Th62;
then A3: N9 is being_line by Th58;
not M // N by A1, Th73;
then not M9 // N9 by Th64;
hence ex p being Element of POS st
( p in M & p in N ) by A2, A3, AFF_1:72; :: thesis: verum