let a, b be Element of L; :: thesis: ( a,b are_orthogonal implies b,a are_orthogonal )
assume a _|_ b ; :: thesis: b,a are_orthogonal
then a [= b ` by Def5;
then (b `) ` [= a ` by Th4;
then b [= a ` by ROBBINS3:def 6;
hence b,a are_orthogonal by Def5; :: thesis: verum