let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; :: thesis: L is join-commutative
let x, y be Element of L; :: according to LATTICES:def 4 :: thesis: x "\/" y = y "\/" x
x "\/" y = (x ") | (y | y) by Def12
.= (y | y) | (x | x) by Th31
.= y "\/" x by Def12 ;
hence x "\/" y = y "\/" x ; :: thesis: verum