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) ) and
A4: r,s _|_ K by A1, Def13;
r,s _|_ N by A2, A4, Th50;
hence N _|_ M by A3, Def13; :: thesis: verum