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 holds (All a,PA,G) 'imp' u '<' Ex (a 'imp' u),PA,G
let a, u be Element of Funcs Y,BOOLEAN ; :: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds (All a,PA,G) 'imp' u '<' Ex (a 'imp' u),PA,G
let G be Subset of (PARTITIONS Y); :: thesis: for PA being a_partition of Y holds (All a,PA,G) 'imp' u '<' Ex (a 'imp' u),PA,G
let PA be a_partition of Y; :: thesis: (All a,PA,G) 'imp' u '<' Ex (a 'imp' u),PA,G
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not K71(Y,BOOLEAN ,((All a,PA,G) 'imp' u),z) = TRUE or K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE )
assume ((All a,PA,G) 'imp' u) . z = TRUE ; :: thesis: K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE
then A1: ('not' ((All a,PA,G) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def 11;
A2: ( 'not' ((All a,PA,G) . z) = TRUE or 'not' ((All a,PA,G) . z) = FALSE ) by XBOOLEAN:def 3;
A3: ( z in EqClass z,(CompF PA,G) & EqClass z,(CompF PA,G) in CompF PA,G ) by EQREL_1:def 8;

now

per cases ( 'not' ((All a,PA,G) . z) = TRUE or u . z = TRUE ) by A1, A2;

case 'not' ((All a,PA,G) . z) = TRUE ; :: thesis: K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE

then consider x1 being Element of Y such that
A4: ( x1 in EqClass z,(CompF PA,G) & a . x1 <> TRUE ) by BVFUNC_1:def 19;

now

assume for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not (a 'imp' u) . x = TRUE ) ; :: thesis: contradiction
then (a 'imp' u) . x1 <> TRUE by A4;
then (a 'imp' u) . x1 = FALSE by XBOOLEAN:def 3;
then A5: ('not' (a . x1)) 'or' (u . x1) = FALSE by BVFUNC_1:def 11;
( 'not' (a . x1) = TRUE or 'not' (a . x1) = FALSE ) by XBOOLEAN:def 3;
hence contradiction by A4, A5; :: thesis: verum

end;

hence K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE by BVFUNC_1:def 20; :: thesis: verum

end;

case A6: u . z = TRUE ; :: thesis: K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE

now

assume for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not (a 'imp' u) . x = TRUE ) ; :: thesis: contradiction
then (a 'imp' u) . z <> TRUE by A3;
then (a 'imp' u) . z = FALSE by XBOOLEAN:def 3;
then ('not' (a . z)) 'or' (u . z) = FALSE by BVFUNC_1:def 11;
hence contradiction by A6; :: thesis: verum

end;

hence K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE by BVFUNC_1:def 20; :: thesis: verum

end;

end;

end;

hence K71(Y,BOOLEAN ,(Ex (a 'imp' u),PA,G),z) = TRUE ; :: thesis: verum