let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN

for G being Subset of (PARTITIONS Y)

for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)

let a be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)

for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)

let G be Subset of (PARTITIONS Y); :: thesis: for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)

let PA, PB be a_partition of Y; :: thesis: All (a,PA,G) '<' Ex (a,PB,G)

( All (a,PA,G) '<' a & a '<' Ex (a,PB,G) ) by BVFUNC_2:11, BVFUNC_2:12;

hence All (a,PA,G) '<' Ex (a,PB,G) by BVFUNC_1:15; :: thesis: verum

for G being Subset of (PARTITIONS Y)

for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)

let a be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)

for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)

let G be Subset of (PARTITIONS Y); :: thesis: for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)

let PA, PB be a_partition of Y; :: thesis: All (a,PA,G) '<' Ex (a,PB,G)

( All (a,PA,G) '<' a & a '<' Ex (a,PB,G) ) by BVFUNC_2:11, BVFUNC_2:12;

hence All (a,PA,G) '<' Ex (a,PB,G) by BVFUNC_1:15; :: thesis: verum