let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for w, p, q being Element of L holds ((q | p) | w) | q = q | ((p | p) | w)
let w, p, q be Element of L; :: thesis: ((q | p) | w) | q = q | ((p | p) | w)
w | (p | q) = (q | p) | w by Th153;
hence ((q | p) | w) | q = q | ((p | p) | w) by Th146; :: thesis: verum