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;

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

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

A5: now :: thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
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;

thus (a 'or' b) . z = (a . z) 'or' (b . z) by BVFUNC_1:def 4
.= TRUE 'or' (b . z) by A2, A5
.= TRUE by BINARITH:10 ; :: thesis: verum

end;

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

A7: now :: thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
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;

thus (a 'or' b) . z = (a . z) 'or' (b . z) by BVFUNC_1:def 4
.= (a . z) 'or' TRUE by A2, A7
.= TRUE by BINARITH:10 ; :: thesis: verum

end;

end;