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 ) )
assume A1: M _|_ N ; :: thesis: ex p being Element of POS st
( p in M & p in N )
then A2: not M // N by Th73;
reconsider M' = M, N' = N as Subset of (Af POS) ;
( M is being_line & N is being_line ) by A1, Th62;
then A3: ( M' is being_line & N' is being_line ) by Th58;
not M' // N' by A2, Th64;
then consider p' being Element of (Af POS) such that
A4: ( p' in M' & p' in N' ) by A3, AFF_1:72;
thus ex p being Element of POS st
( p in M & p in N ) by A4; :: thesis: verum