let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
let a be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
let PA be a_partition of Y; :: thesis: 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y
A1: now :: thesis: ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies for x being Element of Y holds
( not x in EqClass (y,PA) or not ('not' a) . x = TRUE ) )
assume that
A2: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A3: ex x being Element of Y st
( x in EqClass (y,PA) & ('not' a) . x = TRUE ) ; :: thesis: contradiction
consider x1 being Element of Y such that
A4: x1 in EqClass (y,PA) and
A5: ('not' a) . x1 = TRUE by A3;
('not' ('not' a)) . x1 = 'not' TRUE by A5, MARGREL1:def 19;
hence contradiction by A2, A4; :: thesis: verum
end;
A6: now :: thesis: ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies ex x being Element of Y st
( x in EqClass (y,PA) & ('not' a) . x = TRUE ) )
assume that
A7: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A8: for x being Element of Y holds
( not x in EqClass (y,PA) or not ('not' a) . x = TRUE ) ; :: thesis: contradiction
consider x1 being Element of Y such that
A9: x1 in EqClass (y,PA) and
A10: a . x1 <> TRUE by A7;
a . x1 = FALSE by A10, XBOOLEAN:def 3;
then ('not' a) . x1 = 'not' FALSE by MARGREL1:def 19;
hence contradiction by A8, A9; :: thesis: verum
end;
A11: now :: thesis: ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (y,PA) & ('not' a) . x = TRUE ) implies ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y )
assume that
A12: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A13: ex x being Element of Y st
( x in EqClass (y,PA) & ('not' a) . x = TRUE ) ; :: thesis: ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y
(B_INF (a,PA)) . y = FALSE by A12, Def16;
then ('not' (B_INF (a,PA))) . y = 'not' FALSE by MARGREL1:def 19;
hence ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y by A13, Def17; :: thesis: verum
end;
now :: thesis: ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (y,PA) or not ('not' a) . x = TRUE ) ) implies ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y )
assume that
A14: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A15: for x being Element of Y holds
( not x in EqClass (y,PA) or not ('not' a) . x = TRUE ) ; :: thesis: ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y
(B_INF (a,PA)) . y = TRUE by A14, Def16;
then ('not' (B_INF (a,PA))) . y = 'not' TRUE by MARGREL1:def 19;
hence ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y by A15, Def17; :: thesis: verum
end;
hence ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y by A1, A11, A6; :: thesis: verum