let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a, b being Function of 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 Function of 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 Function of 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))
( 'not' (All ((('not' a) 'or' b),PA,G)) = Ex (('not' (('not' a) 'or' b)),PA,G) & 'not' (('not' a) 'or' b) = ('not' ('not' a)) '&' ('not' b) ) by BVFUNC_1:13, BVFUNC_2:18;
hence All ((a 'imp' b),PA,G) = 'not' (Ex ((a '&' ('not' b)),PA,G)) by Th26; :: thesis: verum