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 ;
ex c, d being Element of POS st
( c <> d & M = Line (c,d) & a,b _|_ c,d ) by A2;
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;
hence K _|_ M by A3, A5; :: thesis: verum