let a, b be Element of L; :: thesis: ( (L,a,b) implies (L,b,a) )
( a "/\" b <> Bottom L implies b "/\" a <> Bottom L ) ;
hence ( (L,a,b) implies (L,b,a) ) ; :: thesis: verum