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 by Def14;
p,q _|_ a,b by A2, Def9;
then p,q _|_ b,a by Def9;
then b,a _|_ p,q by Def9;
hence b,a _|_ K by A1, Def14; :: thesis: verum