let POS be non empty ParOrtStr ; :: thesis: for K, M being Subset of POS holds
( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b _|_ c,d ) )
let K, M be Subset of POS; :: thesis: ( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b _|_ c,d ) )

hereby :: thesis: ( ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b _|_ c,d ) implies K _|_ M )

assume K _|_ M ; :: thesis: ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b _|_ c,d )
then consider a, b being Element of POS such that
A1: ( a <> b & K = Line a,b ) and
A2: a,b _|_ M by Def15;
ex c, d being Element of POS st
( c <> d & M = Line c,d & a,b _|_ c,d ) by A2, Def14;
hence ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b _|_ c,d ) by A1; :: thesis: verum

end;

given a, b, c, d being Element of POS such that A3: a <> b and
A4: c <> d and
A5: K = Line a,b and
A6: ( M = Line c,d & a,b _|_ c,d ) ; :: thesis: K _|_ M
a,b _|_ M by A4, A6, Def14;
hence K _|_ M by A3, A5, Def15; :: thesis: verum