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 st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
let a, b be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
let G be Subset of (PARTITIONS Y); :: thesis: for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
let PA be a_partition of Y; :: thesis: ( a 'eqv' b = I_el Y implies (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y )
assume A1: a 'eqv' b = I_el Y ; :: thesis: (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
then b 'imp' a = I_el Y by Th10;
then A2: ('not' b) 'or' a = I_el Y by Th8;
a 'imp' b = I_el Y by A1, Th10;
then A3: ('not' a) 'or' b = I_el Y by Th8;
for z being Element of Y holds ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE

proof

let z be Element of Y; :: thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE

A4: now :: thesis: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) implies ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE )

assume that
A5: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE and
A6: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; :: thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
consider x1 being Element of Y such that
A7: x1 in EqClass (z,(CompF (PA,G))) and
A8: b . x1 <> TRUE by A6;
A9: a . x1 = TRUE by A5, A7;
A10: b . x1 = FALSE by A8, XBOOLEAN:def 3;
(('not' a) 'or' b) . x1 = (('not' a) . x1) 'or' (b . x1) by BVFUNC_1:def 4
.= FALSE 'or' FALSE by A10, A9, MARGREL1:def 19
.= FALSE ;
hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A3, BVFUNC_1:def 11; :: thesis: verum

end;

A11: now :: thesis: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) implies ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE )

assume that
A12: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) and
A13: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ; :: thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
consider x1 being Element of Y such that
A14: x1 in EqClass (z,(CompF (PA,G))) and
A15: a . x1 <> TRUE by A12;
A16: b . x1 = TRUE by A13, A14;
A17: a . x1 = FALSE by A15, XBOOLEAN:def 3;
(('not' b) 'or' a) . x1 = (('not' b) . x1) 'or' (a . x1) by BVFUNC_1:def 4
.= FALSE 'or' FALSE by A17, A16, MARGREL1:def 19
.= FALSE ;
hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, BVFUNC_1:def 11; :: thesis: verum

end;

(All (a,PA,G)) 'eqv' (All (b,PA,G)) = ((All (a,PA,G)) 'imp' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) by Th7
.= (('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) by Th8
.= (('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (('not' (All (b,PA,G))) 'or' (All (a,PA,G))) by Th8
.= ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G))) by BVFUNC_1:12
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G))))) 'or' ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G))) by BVFUNC_1:12
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G))))) 'or' ((('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by BVFUNC_1:12
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y)) 'or' ((('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by Th5
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y)) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by Th5
.= (('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by BVFUNC_1:9
.= (('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G))) by BVFUNC_1:9 ;
then A18: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) by BVFUNC_1:def 4
.= ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) by MARGREL1:def 20
.= ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def 20
.= (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def 19
.= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def 19 ;

A19: now :: thesis: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) implies ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE )

assume that
A20: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) and
A21: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; :: thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
(B_INF (b,(CompF (PA,G)))) . z = FALSE by A21, BVFUNC_1:def 16;
hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A18, A20, BVFUNC_1:def 16; :: thesis: verum

end;

now :: thesis: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) implies ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE )

assume that
A22: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE and
A23: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ; :: thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
(B_INF (b,(CompF (PA,G)))) . z = TRUE by A23, BVFUNC_1:def 16;
hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A18, A22, BVFUNC_1:def 16; :: thesis: verum

end;

hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A4, A11, A19; :: thesis: verum

end;

hence (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y by BVFUNC_1:def 11; :: thesis: verum