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 ) ) )
for a, b being Element of POS
for K being Subset of POS st a,b _|_ K holds
K is being_line ;
then ( K _|_ M implies ( K is being_line & M is being_line ) ) ;
hence ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) ) ; :: thesis: verum