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
All a,P,G '<' All 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
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
A2: All a,P,G = B_INF a,(CompF P,G) by BVFUNC_2:def 9;
A3: All b,P,G = B_INF b,(CompF P,G) by BVFUNC_2:def 9;
let x be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not (All a,P,G) . x = TRUE or (All b,P,G) . x = TRUE )
assume A4: (All a,P,G) . x = TRUE ; :: thesis: (All b,P,G) . x = TRUE
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 A2, A4, BVFUNC_1:def 19;
hence b . y = TRUE by A1, BVFUNC_1:def 15; :: thesis: verum

end;

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