let Y be non empty set ; :: thesis: for a, b being Element of Funcs 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 Element of Funcs 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:13;
All b,A,G '<' Ex b,A,G by BVFUNC_4:18;
hence All a,A,G '<' Ex b,A,G by A1, BVFUNC_1:18; :: thesis: verum