let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; :: thesis: L is meet-commutative

let x, y be Element of L; :: according to LATTICES:def 6 :: thesis: x "/\" y = y "/\" x

x "/\" y = (x | y) | (x | y) by Def12

.= (y | x) | (x | y) by Th31

.= (y | x) | (y | x) by Th31

.= y "/\" x by Def12 ;

hence x "/\" y = y "/\" x ; :: thesis: verum

let x, y be Element of L; :: according to LATTICES:def 6 :: thesis: x "/\" y = y "/\" x

x "/\" y = (x | y) | (x | y) by Def12

.= (y | x) | (x | y) by Th31

.= (y | x) | (y | x) by Th31

.= y "/\" x by Def12 ;

hence x "/\" y = y "/\" x ; :: thesis: verum