let Y be non empty set ; :: thesis: 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 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let a, b be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let G be Subset of (PARTITIONS Y); :: thesis: for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let PA be a_partition of Y; :: thesis: All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let z be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (All ((a 'eqv' b),PA,G)) . z = ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z
(All ((a 'eqv' b),PA,G)) . z = (All (((a 'imp' b) '&' (b 'imp' a)),PA,G)) . z by Th7
.= ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z by BVFUNC_1:39 ;
hence (All ((a 'eqv' b),PA,G)) . z = ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z ; :: thesis: verum