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

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

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

All (b,P,G) = B_INF (b,(CompF (P,G)))
by BVFUNC_2:def 9;
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;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

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