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

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