let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; :: thesis: ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
( ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) & ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) '<' ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) ) by Lm2;
hence ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) by BVFUNC_1:15; :: thesis: verum