let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)

for a, b being Function of Y,BOOLEAN

for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let G be Subset of (PARTITIONS Y); :: thesis: for a, b being Function of Y,BOOLEAN

for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let a, b be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let PA be a_partition of Y; :: thesis: (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE or (a 'or' b) . z = TRUE )

A1: ( (All (a,PA,G)) . z = TRUE or (All (a,PA,G)) . z = FALSE ) by XBOOLEAN:def 3;

A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def 6;

assume ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE ; :: thesis: (a 'or' b) . z = TRUE

then A3: ((All (a,PA,G)) . z) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def 4;

for a, b being Function of Y,BOOLEAN

for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let G be Subset of (PARTITIONS Y); :: thesis: for a, b being Function of Y,BOOLEAN

for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let a, b be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let PA be a_partition of Y; :: thesis: (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b

let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE or (a 'or' b) . z = TRUE )

A1: ( (All (a,PA,G)) . z = TRUE or (All (a,PA,G)) . z = FALSE ) by XBOOLEAN:def 3;

A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def 6;

assume ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE ; :: thesis: (a 'or' b) . z = TRUE

then A3: ((All (a,PA,G)) . z) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def 4;

per cases
( (All (a,PA,G)) . z = TRUE or (All (b,PA,G)) . z = TRUE )
by A3, A1, BINARITH:3;

end;

suppose A4:
(All (a,PA,G)) . z = TRUE
; :: thesis: (a 'or' b) . z = TRUE

.= TRUE 'or' (b . z) by A2, A5

.= TRUE by BINARITH:10 ; :: thesis: verum

end;

A5: now :: thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds

a . x = TRUE

thus (a 'or' b) . z =
(a . z) 'or' (b . z)
by BVFUNC_1:def 4
a . x = TRUE

assume
ex x being Element of Y st

( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; :: thesis: contradiction

then (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 16;

hence contradiction by A4, BVFUNC_2:def 9; :: thesis: verum

end;( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; :: thesis: contradiction

then (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 16;

hence contradiction by A4, BVFUNC_2:def 9; :: thesis: verum

.= TRUE 'or' (b . z) by A2, A5

.= TRUE by BINARITH:10 ; :: thesis: verum

suppose A6:
(All (b,PA,G)) . z = TRUE
; :: thesis: (a 'or' b) . z = TRUE

.= (a . z) 'or' TRUE by A2, A7

.= TRUE by BINARITH:10 ; :: thesis: verum

end;

A7: now :: thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds

b . x = TRUE

thus (a 'or' b) . z =
(a . z) 'or' (b . z)
by BVFUNC_1:def 4
b . x = TRUE

assume
ex x being Element of Y st

( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; :: thesis: contradiction

then (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 16;

hence contradiction by A6, BVFUNC_2:def 9; :: thesis: verum

end;( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; :: thesis: contradiction

then (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 16;

hence contradiction by A6, BVFUNC_2:def 9; :: thesis: verum

.= (a . z) 'or' TRUE by A2, A7

.= TRUE by BINARITH:10 ; :: thesis: verum