let Y be non empty set ; for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let a, b be Function of Y,BOOLEAN; for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let G be Subset of (PARTITIONS Y); for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let PA be a_partition of Y; All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let z be Element of Y; BVFUNC_1:def 12 ( not (All ((a '&' b),PA,G)) . z = TRUE or (a '&' (All (b,PA,G))) . z = TRUE )
assume A1:
(All ((a '&' b),PA,G)) . z = TRUE
; (a '&' (All (b,PA,G))) . z = TRUE
then A9:
(B_INF (b,(CompF (PA,G)))) . z = TRUE
by BVFUNC_1:def 16;
z in EqClass (z,(CompF (PA,G)))
by EQREL_1:def 6;
then
a . z = TRUE
by A2;
then (a '&' (All (b,PA,G))) . z =
TRUE '&' TRUE
by A9, MARGREL1:def 20
.=
TRUE
;
hence
(a '&' (All (b,PA,G))) . z = TRUE
; verum