let Y be non empty set ; :: thesis: for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
let a, u be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
let G be Subset of (PARTITIONS Y); :: thesis: for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
let PA be a_partition of Y; :: thesis: ( a 'imp' u = I_el Y implies (All (a,PA,G)) 'imp' u = I_el Y )
assume A1: a 'imp' u = I_el Y ; :: thesis: (All (a,PA,G)) 'imp' u = I_el Y
for x being Element of Y holds ((All (a,PA,G)) 'imp' u) . x = TRUE

proof

let x be Element of Y; :: thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE
(a 'imp' u) . x = TRUE by A1, BVFUNC_1:def 11;
then A2: ('not' (a . x)) 'or' (u . x) = TRUE by BVFUNC_1:def 8;
A3: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def 3;

now :: thesis: ( ( 'not' (a . x) = TRUE & ((All (a,PA,G)) 'imp' u) . x = TRUE ) or ( u . x = TRUE & ((All (a,PA,G)) 'imp' u) . x = TRUE ) )

per cases ( 'not' (a . x) = TRUE or u . x = TRUE ) by A2, A3;

case A4: 'not' (a . x) = TRUE ; :: thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE

x in EqClass (x,(CompF (PA,G))) by EQREL_1:def 6;
then (B_INF (a,(CompF (PA,G)))) . x = FALSE by A4, BVFUNC_1:def 16;
then ((All (a,PA,G)) 'imp' u) . x = TRUE 'or' (u . x) by BVFUNC_1:def 8
.= TRUE ;
hence ((All (a,PA,G)) 'imp' u) . x = TRUE ; :: thesis: verum

end;

case u . x = TRUE ; :: thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE

then ((All (a,PA,G)) 'imp' u) . x = ('not' ((All (a,PA,G)) . x)) 'or' TRUE by BVFUNC_1:def 8
.= TRUE ;
hence ((All (a,PA,G)) 'imp' u) . x = TRUE ; :: thesis: verum

end;

end;

end;

hence ((All (a,PA,G)) 'imp' u) . x = TRUE ; :: thesis: verum

end;

hence (All (a,PA,G)) 'imp' u = I_el Y by BVFUNC_1:def 11; :: thesis: verum