let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A being a_partition of Y st a '<' b holds
All (a,A,G) '<' Ex (b,A,G)
let a, b be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for A being a_partition of Y st a '<' b holds
All (a,A,G) '<' Ex (b,A,G)
let G be Subset of (PARTITIONS Y); :: thesis: for A being a_partition of Y st a '<' b holds
All (a,A,G) '<' Ex (b,A,G)
let A be a_partition of Y; :: thesis: ( a '<' b implies All (a,A,G) '<' Ex (b,A,G) )
assume a '<' b ; :: thesis: All (a,A,G) '<' Ex (b,A,G)
then A1: All (a,A,G) '<' All (b,A,G) by PARTIT_2:12;
All (b,A,G) '<' Ex (b,A,G) by BVFUNC_4:17;
hence All (a,A,G) '<' Ex (b,A,G) by A1, BVFUNC_1:15; :: thesis: verum