let Y be non empty set ; :: thesis: for a, u being Function of Y,BOOLEAN
for G being Subset of ()
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 ()
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 (); :: 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 ;
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 ;
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