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 | (x | x) = y | (y | y)

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

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

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

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

.= ((y | (y ")) ") " by Def14

.= y | (y | y) by Def13 ;

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

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

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

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

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

.= ((y | (y ")) ") " by Def14

.= y | (y | y) by Def13 ;

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