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
All (a,P,G) '<' All (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
All (a,P,G) '<' All (b,P,G)
let G be Subset of (PARTITIONS Y); :: thesis: for P being a_partition of Y st a '<' b holds
All (a,P,G) '<' All (b,P,G)
let P be a_partition of Y; :: thesis: ( a '<' b implies All (a,P,G) '<' All (b,P,G) )
assume A1: a '<' b ; :: thesis: All (a,P,G) '<' All (b,P,G)
let x be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (All (a,P,G)) . x = TRUE or (All (b,P,G)) . x = TRUE )
assume A2: (All (a,P,G)) . x = TRUE ; :: thesis: (All (b,P,G)) . x = TRUE
A3: All (a,P,G) = B_INF (a,(CompF (P,G))) by BVFUNC_2:def 9;
A4: for y being Element of Y st y in EqClass (x,(CompF (P,G))) holds
b . y = TRUE

proof

let y be Element of Y; :: thesis: ( y in EqClass (x,(CompF (P,G))) implies b . y = TRUE )
assume y in EqClass (x,(CompF (P,G))) ; :: thesis: b . y = TRUE
then a . y = TRUE by A3, A2, BVFUNC_1:def 16;
hence b . y = TRUE by A1; :: thesis: verum

end;

All (b,P,G) = B_INF (b,(CompF (P,G))) by BVFUNC_2:def 9;
hence (All (b,P,G)) . x = TRUE by A4, BVFUNC_1:def 16; :: thesis: verum