let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(Ex a,PA,G) 'eqv' (Ex b,PA,G) = I_el Y
let a, b be Element of Funcs 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
(Ex a,PA,G) 'eqv' (Ex 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
(Ex a,PA,G) 'eqv' (Ex b,PA,G) = I_el Y
let PA be a_partition of Y; :: thesis: ( a 'eqv' b = I_el Y implies (Ex a,PA,G) 'eqv' (Ex b,PA,G) = I_el Y )
assume A1: a 'eqv' b = I_el Y ; :: thesis: (Ex a,PA,G) 'eqv' (Ex 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 ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE

proof

let z be Element of Y; :: thesis: ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE
(Ex a,PA,G) 'eqv' (Ex b,PA,G) = ((Ex a,PA,G) 'imp' (Ex b,PA,G)) '&' ((Ex b,PA,G) 'imp' (Ex a,PA,G)) by Th7
.= (('not' (Ex a,PA,G)) 'or' (Ex b,PA,G)) '&' ((Ex b,PA,G) 'imp' (Ex a,PA,G)) by Th8
.= (('not' (Ex a,PA,G)) 'or' (Ex b,PA,G)) '&' (('not' (Ex b,PA,G)) 'or' (Ex a,PA,G)) by Th8
.= ((('not' (Ex a,PA,G)) 'or' (Ex b,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' ((('not' (Ex a,PA,G)) 'or' (Ex b,PA,G)) '&' (Ex a,PA,G)) by BVFUNC_1:15
.= ((('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' ((Ex b,PA,G) '&' ('not' (Ex b,PA,G)))) 'or' ((('not' (Ex a,PA,G)) 'or' (Ex b,PA,G)) '&' (Ex a,PA,G)) by BVFUNC_1:15
.= ((('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' ((Ex b,PA,G) '&' ('not' (Ex b,PA,G)))) 'or' ((('not' (Ex a,PA,G)) '&' (Ex a,PA,G)) 'or' ((Ex b,PA,G) '&' (Ex a,PA,G))) by BVFUNC_1:15
.= ((('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' (O_el Y)) 'or' ((('not' (Ex a,PA,G)) '&' (Ex a,PA,G)) 'or' ((Ex b,PA,G) '&' (Ex a,PA,G))) by Th5
.= ((('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' (O_el Y)) 'or' ((O_el Y) 'or' ((Ex b,PA,G) '&' (Ex a,PA,G))) by Th5
.= (('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' ((O_el Y) 'or' ((Ex b,PA,G) '&' (Ex a,PA,G))) by BVFUNC_1:12
.= (('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) 'or' ((Ex b,PA,G) '&' (Ex a,PA,G)) by BVFUNC_1:12 ;
then A4: ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = ((('not' (Ex a,PA,G)) '&' ('not' (Ex b,PA,G))) . z) 'or' (((Ex b,PA,G) '&' (Ex a,PA,G)) . z) by BVFUNC_1:def 7
.= ((('not' (Ex a,PA,G)) . z) '&' (('not' (Ex b,PA,G)) . z)) 'or' (((Ex b,PA,G) '&' (Ex a,PA,G)) . z) by MARGREL1:def 21
.= ((('not' (Ex a,PA,G)) . z) '&' (('not' (Ex b,PA,G)) . z)) 'or' (((Ex b,PA,G) . z) '&' ((Ex a,PA,G) . z)) by MARGREL1:def 21
.= (('not' ((Ex a,PA,G) . z)) '&' (('not' (Ex b,PA,G)) . z)) 'or' (((Ex b,PA,G) . z) '&' ((Ex a,PA,G) . z)) by MARGREL1:def 20
.= (('not' ((Ex a,PA,G) . z)) '&' ('not' ((Ex b,PA,G) . z))) 'or' (((Ex b,PA,G) . z) '&' ((Ex a,PA,G) . z)) by MARGREL1:def 20 ;

per cases ( ( ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & b . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not b . x = TRUE ) ) ) or ( ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & b . x = TRUE ) ) or ( ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not b . x = TRUE ) ) ) ) ;

suppose A5: ( ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & b . x = TRUE ) ) ; :: thesis: ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE

then (B_SUP b,(CompF PA,G)) . z = TRUE by BVFUNC_1:def 20;
hence ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE by A4, A5, BVFUNC_1:def 20; :: thesis: verum

end;

suppose A6: ( ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not b . x = TRUE ) ) ) ; :: thesis: ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE

then consider x1 being Element of Y such that
A7: x1 in EqClass z,(CompF PA,G) and
A8: a . x1 = TRUE ;
b . x1 <> TRUE by A6, A7;
then A9: b . x1 = FALSE by XBOOLEAN:def 3;
(('not' a) 'or' b) . x1 = (('not' a) . x1) 'or' (b . x1) by BVFUNC_1:def 7
.= FALSE 'or' FALSE by A8, A9, MARGREL1:def 20
.= FALSE ;
hence ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE by A3, BVFUNC_1:def 14; :: thesis: verum

end;

suppose A10: ( ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass z,(CompF PA,G) & b . x = TRUE ) ) ; :: thesis: ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE

then consider x1 being Element of Y such that
A11: x1 in EqClass z,(CompF PA,G) and
A12: b . x1 = TRUE ;
a . x1 <> TRUE by A10, A11;
then A13: a . x1 = FALSE by XBOOLEAN:def 3;
(('not' b) 'or' a) . x1 = (('not' b) . x1) 'or' (a . x1) by BVFUNC_1:def 7
.= FALSE 'or' FALSE by A12, A13, MARGREL1:def 20
.= FALSE ;
hence ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE by A2, BVFUNC_1:def 14; :: thesis: verum

end;

suppose A14: ( ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass z,(CompF PA,G) or not b . x = TRUE ) ) ) ; :: thesis: ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE

then (B_SUP b,(CompF PA,G)) . z = FALSE by BVFUNC_1:def 20;
hence ((Ex a,PA,G) 'eqv' (Ex b,PA,G)) . z = TRUE by A4, A14, BVFUNC_1:def 20; :: thesis: verum

end;

end;

end;

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