let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; :: thesis: for x, y being Element of L holds x | y = y | x

let x, y be Element of L; :: thesis: x | y = y | x

x | y = ((x | y) ") " by Def13

.= ((x | ((y ") ")) ") " by Def13

.= ((((y ") ") | x) ") " by Def15

.= ((y | x) ") " by Def13

.= y | x by Def13 ;

hence x | y = y | x ; :: thesis: verum

let x, y be Element of L; :: thesis: x | y = y | x

x | y = ((x | y) ") " by Def13

.= ((x | ((y ") ")) ") " by Def13

.= ((((y ") ") | x) ") " by Def15

.= ((y | x) ") " by Def13

.= y | x by Def13 ;

hence x | y = y | x ; :: thesis: verum