let POS be OrtAfSp; :: thesis: for K, M, N being Subset of POS st K _|_ M & K // N holds
N _|_ M
let K, M, N be Subset of POS; :: thesis: ( K _|_ M & K // N implies N _|_ M )
assume that
A1: K _|_ M and
A2: K // N ; :: thesis: N _|_ M
consider r, s being Element of POS such that
A3: ( r <> s & M = Line r,s & r,s _|_ K ) by A1, Def15;
r,s _|_ N by A2, A3, Th69;
hence N _|_ M by A3, Def15; :: thesis: verum