let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let a, b be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let PA be a_partition of Y; :: thesis: B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

A5: now :: thesis: ( ex x being Element of Y st
( x in EqClass (y,PA) & (a 'or' b) . x = TRUE ) implies (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y )

assume A6: ex x being Element of Y st
( x in EqClass (y,PA) & (a 'or' b) . x = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
then consider x1 being Element of Y such that
A7: x1 in EqClass (y,PA) and
A8: (a 'or' b) . x1 = TRUE ;
A9: ( ( a . x1 = FALSE & b . x1 = FALSE ) or ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by XBOOLEAN:def 3;
A10: (a . x1) 'or' (b . x1) = TRUE by A8, Def4;

now :: thesis: ( ( a . x1 = FALSE & b . x1 = TRUE & (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ) or ( a . x1 = TRUE & b . x1 = FALSE & (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ) or ( a . x1 = TRUE & b . x1 = TRUE & (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ) )

per cases ( ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by A10, A9;

case ( a . x1 = FALSE & b . x1 = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

then (B_SUP (b,PA)) . y = TRUE by A7, Def17;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def17; :: thesis: verum

end;

case ( a . x1 = TRUE & b . x1 = FALSE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

then (B_SUP (a,PA)) . y = TRUE by A7, Def17;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def17; :: thesis: verum

end;

case ( a . x1 = TRUE & b . x1 = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

then (B_SUP (b,PA)) . y = TRUE by A7, Def17;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def17; :: thesis: verum

end;

end;

end;

hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ; :: thesis: verum

end;

now :: thesis: ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not (a 'or' b) . x = TRUE ) ) implies (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y )

assume A11: for x being Element of Y holds
( not x in EqClass (y,PA) or not (a 'or' b) . x = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

now :: thesis: for x being Element of Y holds
( not x in EqClass (y,PA) or not b . x = TRUE )

assume ex x being Element of Y st
( x in EqClass (y,PA) & b . x = TRUE ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A12: x1 in EqClass (y,PA) and
A13: b . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A13;
then (a 'or' b) . x1 = TRUE by Def4;
hence contradiction by A11, A12; :: thesis: verum

end;

then A14: (B_SUP (b,PA)) . y = FALSE by Def17;

now :: thesis: for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE )

assume ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A15: x1 in EqClass (y,PA) and
A16: a . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A16;
then (a 'or' b) . x1 = TRUE by Def4;
hence contradiction by A11, A15; :: thesis: verum

end;

then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = FALSE 'or' FALSE by A14, Def17;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = FALSE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A11, Def17; :: thesis: verum

end;

hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A5; :: thesis: verum