let Y be non empty set ; 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); 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; 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; (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b
let z be Element of Y; BVFUNC_1:def 12 ( 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
; (a 'or' b) . z = TRUE
then A3:
((All (a,PA,G)) . z) 'or' ((All (b,PA,G)) . z) = TRUE
by BVFUNC_1:def 4;