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 AffinStruct(# the carrier of POS, the CONGR of POS #) ;
assume A1: M _|_ N ; :: thesis: ex p being Element of POS st
( p in M & p in N )
then M is being_line ;
then A2: M9 is being_line by Th43;
N is being_line by A1, Th44;
then A3: N9 is being_line by Th43;
not M // N by A1, Th52;
then not M9 // N9 by Th46;
hence ex p being Element of POS st
( p in M & p in N ) by A2, A3, AFF_1:58; :: thesis: verum