let POS be non empty ParOrtStr ; :: thesis: for a, b being Element of POS
for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
let a, b be Element of POS; :: thesis: for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
let K, M be Subset of POS; :: thesis: ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )

A1: now

let a, b be Element of POS; :: thesis: for K being Subset of POS st a,b _|_ K holds
K is being_line
let K be Subset of POS; :: thesis: ( a,b _|_ K implies K is being_line )
assume a,b _|_ K ; :: thesis: K is being_line
then ex p, q being Element of POS st
( p <> q & K = Line p,q & a,b _|_ p,q ) by Def14;
hence K is being_line by Def13; :: thesis: verum

end;

now

assume K _|_ M ; :: thesis: ( K is being_line & M is being_line )
then A2: ex p, q being Element of POS st
( p <> q & K = Line p,q & p,q _|_ M ) by Def15;
hence K is being_line by Def13; :: thesis: M is being_line
thus M is being_line by A1, A2; :: thesis: verum

end;

hence ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) ) by A1; :: thesis: verum