let POS be OrtAfSp; :: thesis: for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
let K be Subset of POS; :: thesis: for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
let a, b be Element of POS; :: thesis: ( a,b _|_ K implies b,a _|_ K )
assume a,b _|_ K ; :: thesis: b,a _|_ K
then consider p, q being Element of POS such that
A1: ( p <> q & K = Line (p,q) ) and
A2: a,b _|_ p,q ;
p,q _|_ a,b by A2, Def7;
then p,q _|_ b,a by Def7;
then b,a _|_ p,q by Def7;
hence b,a _|_ K by A1; :: thesis: verum