let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for a, b, c being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); for a, b, c being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let a, b, c be Function of Y,BOOLEAN; for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let PA be a_partition of Y; (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let z be Element of Y; BVFUNC_1:def 12 ( not ((All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G))) . z = TRUE or (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE )
assume
((All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G))) . z = TRUE
; (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE
then A1:
((All ((b 'imp' ('not' c)),PA,G)) . z) '&' ((All ((a 'imp' c),PA,G)) . z) = TRUE
by MARGREL1:def 20;
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' ('not' b)) . x = TRUE
then
(B_INF ((a 'imp' ('not' b)),(CompF (PA,G)))) . z = TRUE
by BVFUNC_1:def 16;
hence
(All ((a 'imp' ('not' b)),PA,G)) . z = TRUE
by BVFUNC_2:def 9; verum