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