let Y be non empty set ; :: thesis: for a, b being Element of Funcs 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 Element of Funcs 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:20 ;
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 Th13;
Ex a,P,G = Ex ('not' ('not' a)),P,G
.= 'not' (All ('not' a),P,G) by BVFUNC_2:20 ;
hence Ex a,P,G '<' Ex b,P,G by A1, A2, Th11; :: thesis: verum