let Y be non empty set ; :: thesis: for a, u being Element of Funcs 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 Element of Funcs 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 14;
then A2: ('not' (a . x)) 'or' (u . x) = TRUE by BVFUNC_1:def 11;
A3: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def 3;

now

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 8;
then (B_INF a,(CompF PA,G)) . x = FALSE by A4, BVFUNC_1:def 19;
then ((All a,PA,G) 'imp' u) . x = TRUE 'or' (u . x) by BVFUNC_1:def 11
.= 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 11
.= 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 14; :: thesis: verum