let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
let a, b be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
let G be Subset of (PARTITIONS Y); :: thesis: for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
let P be a_partition of Y; :: thesis: ( a '<' b implies Ex (a,P,G) '<' Ex (b,P,G) )
A1: Ex (b,P,G) = Ex (('not' ('not' b)),P,G)
.= 'not' (All (('not' b),P,G)) by BVFUNC_2:18 ;
assume a '<' b ; :: thesis: Ex (a,P,G) '<' Ex (b,P,G)
then 'not' b '<' 'not' a by Th11;
then A2: All (('not' b),P,G) '<' All (('not' a),P,G) by Th12;
Ex (a,P,G) = Ex (('not' ('not' a)),P,G)
.= 'not' (All (('not' a),P,G)) by BVFUNC_2:18 ;
hence Ex (a,P,G) '<' Ex (b,P,G) by A1, A2, Th11; :: thesis: verum