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