let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All (a 'imp' b),PA,G = 'not' (Ex (a '&' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); :: thesis: for a, b being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All (a 'imp' b),PA,G = 'not' (Ex (a '&' ('not' b)),PA,G)
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y holds All (a 'imp' b),PA,G = 'not' (Ex (a '&' ('not' b)),PA,G)
let PA be a_partition of Y; :: thesis: All (a 'imp' b),PA,G = 'not' (Ex (a '&' ('not' b)),PA,G)
A1: 'not' (All (('not' a) 'or' b),PA,G) = Ex ('not' (('not' a) 'or' b)),PA,G by BVFUNC_2:20;
'not' (('not' a) 'or' b) = ('not' ('not' a)) '&' ('not' b) by BVFUNC_1:16;
hence All (a 'imp' b),PA,G = 'not' (Ex (a '&' ('not' b)),PA,G) by A1, Th26; :: thesis: verum