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