let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN holds
( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )

A1: now

assume A2: for x being Element of Y holds (a '&' b) . x = TRUE ; :: thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
A3: for x being Element of Y holds a . x = TRUE

proof

let x be Element of Y; :: thesis: a . x = TRUE
(a '&' b) . x = (a . x) '&' (b . x) by MARGREL1:def 21;
then (a . x) '&' (b . x) = TRUE by A2;
hence a . x = TRUE by XBOOLEAN:101; :: thesis: verum

end;

A4: for x being Element of Y holds b . x = TRUE

proof

let x be Element of Y; :: thesis: b . x = TRUE
(a '&' b) . x = TRUE by A2;
then (a . x) '&' (b . x) = TRUE by MARGREL1:def 21;
hence b . x = TRUE by XBOOLEAN:101; :: thesis: verum

end;

then A5: (B_INF a) '&' (B_INF b) = (B_INF a) '&' (I_el Y) by Def16
.= (I_el Y) '&' (I_el Y) by A3, Def16 ;
A6: not for x being Element of Y holds (a 'or' b) . x = FALSE

proof

now

assume for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds (a 'or' b) . x = FALSE
let x be Element of Y; :: thesis: not for x being Element of Y holds (a 'or' b) . x = FALSE
A7: (a 'or' b) . x = (a . x) 'or' (b . x) by Def7;
a . x = TRUE by A3;
hence not for x being Element of Y holds (a 'or' b) . x = FALSE by A7; :: thesis: verum

end;

hence not for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis: verum

end;

A8: not for x being Element of Y holds a . x = FALSE

proof

now

assume for x being Element of Y holds a . x = FALSE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds a . x = FALSE
let x be Element of Y; :: thesis: not for x being Element of Y holds a . x = FALSE
a . x = TRUE by A3;
hence not for x being Element of Y holds a . x = FALSE ; :: thesis: verum

end;

hence not for x being Element of Y holds a . x = FALSE ; :: thesis: verum

end;

A9: not for x being Element of Y holds b . x = FALSE

proof

now

assume for x being Element of Y holds b . x = FALSE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds b . x = FALSE
let x be Element of Y; :: thesis: not for x being Element of Y holds b . x = FALSE
b . x = TRUE by A4;
hence not for x being Element of Y holds b . x = FALSE ; :: thesis: verum

end;

hence not for x being Element of Y holds b . x = FALSE ; :: thesis: verum

end;

B_SUP a = I_el Y by A8, Def17;
then (B_SUP a) 'or' (B_SUP b) = (I_el Y) 'or' (I_el Y) by A9, Def17;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A2, A5, A6, Def16, Def17; :: thesis: verum

end;

A10: now

assume A11: for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
A12: for x being Element of Y holds a . x = FALSE

proof

let x be Element of Y; :: thesis: a . x = FALSE
(a 'or' b) . x = FALSE by A11;
then A13: (a . x) 'or' (b . x) = FALSE by Def7;
( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def 3;
hence a . x = FALSE by A13; :: thesis: verum

end;

A14: for x being Element of Y holds b . x = FALSE

proof

let x be Element of Y; :: thesis: b . x = FALSE
(a 'or' b) . x = FALSE by A11;
then A15: (a . x) 'or' (b . x) = FALSE by Def7;
( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def 3;
hence b . x = FALSE by A15; :: thesis: verum

end;

then B_SUP b = O_el Y by Def17;
then A16: (B_SUP a) 'or' (B_SUP b) = (O_el Y) 'or' (O_el Y) by A12, Def17;
A17: not for x being Element of Y holds (a '&' b) . x = TRUE

proof

now

assume for x being Element of Y holds (a '&' b) . x = TRUE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds (a '&' b) . x = TRUE
let x be Element of Y; :: thesis: not for x being Element of Y holds (a '&' b) . x = TRUE
A18: (a '&' b) . x = (a . x) '&' (b . x) by MARGREL1:def 21;
a . x = FALSE by A12;
hence not for x being Element of Y holds (a '&' b) . x = TRUE by A18; :: thesis: verum

end;

hence not for x being Element of Y holds (a '&' b) . x = TRUE ; :: thesis: verum

end;

A19: not for x being Element of Y holds a . x = TRUE

proof

now

assume for x being Element of Y holds a . x = TRUE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds a . x = TRUE
let x be Element of Y; :: thesis: not for x being Element of Y holds a . x = TRUE
a . x = FALSE by A12;
hence not for x being Element of Y holds a . x = TRUE ; :: thesis: verum

end;

hence not for x being Element of Y holds a . x = TRUE ; :: thesis: verum

end;

A20: not for x being Element of Y holds b . x = TRUE

proof

now

assume for x being Element of Y holds b . x = TRUE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds b . x = TRUE
let x be Element of Y; :: thesis: not for x being Element of Y holds b . x = TRUE
b . x = FALSE by A14;
hence not for x being Element of Y holds b . x = TRUE ; :: thesis: verum

end;

hence not for x being Element of Y holds b . x = TRUE ; :: thesis: verum

end;

B_INF a = O_el Y by A19, Def16;
then (B_INF a) '&' (B_INF b) = (O_el Y) '&' (O_el Y) by A20, Def16;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A11, A16, A17, Def16, Def17; :: thesis: verum

end;

now

assume A21: ( not for x being Element of Y holds (a '&' b) . x = TRUE & not for x being Element of Y holds (a 'or' b) . x = FALSE ) ; :: thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
A22: ( ( for x being Element of Y holds (a '&' b) . x = TRUE ) iff ( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds b . x = TRUE ) ) )

proof

A23: ( ( for x being Element of Y holds (a '&' b) . x = TRUE ) implies for x being Element of Y holds a . x = TRUE )

proof

assume A24: for x being Element of Y holds (a '&' b) . x = TRUE ; :: thesis: for x being Element of Y holds a . x = TRUE
let x be Element of Y; :: thesis: a . x = TRUE
(a '&' b) . x = (a . x) '&' (b . x) by MARGREL1:def 21;
then (a . x) '&' (b . x) = TRUE by A24;
hence a . x = TRUE by XBOOLEAN:101; :: thesis: verum

end;

A25: ( ( for x being Element of Y holds (a '&' b) . x = TRUE ) implies for x being Element of Y holds b . x = TRUE )

proof

assume A26: for x being Element of Y holds (a '&' b) . x = TRUE ; :: thesis: for x being Element of Y holds b . x = TRUE
let x be Element of Y; :: thesis: b . x = TRUE
(a '&' b) . x = TRUE by A26;
then (a . x) '&' (b . x) = TRUE by MARGREL1:def 21;
hence b . x = TRUE by XBOOLEAN:101; :: thesis: verum

end;

( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds b . x = TRUE ) implies for x being Element of Y holds (a '&' b) . x = TRUE )

proof

assume A27: ( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds b . x = TRUE ) ) ; :: thesis: for x being Element of Y holds (a '&' b) . x = TRUE
let x be Element of Y; :: thesis: (a '&' b) . x = TRUE
a . x = TRUE by A27;
then (a . x) '&' (b . x) = TRUE by A27;
hence (a '&' b) . x = TRUE by MARGREL1:def 21; :: thesis: verum

end;

hence ( ( for x being Element of Y holds (a '&' b) . x = TRUE ) iff ( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds b . x = TRUE ) ) ) by A23, A25; :: thesis: verum

end;

( ( for x being Element of Y holds (a 'or' b) . x = FALSE ) iff ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds b . x = FALSE ) ) )

proof

A28: ( ( for x being Element of Y holds (a 'or' b) . x = FALSE ) implies for x being Element of Y holds a . x = FALSE )

proof

assume A29: for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis: for x being Element of Y holds a . x = FALSE
let x be Element of Y; :: thesis: a . x = FALSE
(a 'or' b) . x = FALSE by A29;
then A30: (a . x) 'or' (b . x) = FALSE by Def7;
( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def 3;
hence a . x = FALSE by A30; :: thesis: verum

end;

A31: ( ( for x being Element of Y holds (a 'or' b) . x = FALSE ) implies for x being Element of Y holds b . x = FALSE )

proof

assume A32: for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis: for x being Element of Y holds b . x = FALSE
let x be Element of Y; :: thesis: b . x = FALSE
(a 'or' b) . x = FALSE by A32;
then A33: (a . x) 'or' (b . x) = FALSE by Def7;
( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def 3;
hence b . x = FALSE by A33; :: thesis: verum

end;

( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds b . x = FALSE ) implies for x being Element of Y holds (a 'or' b) . x = FALSE )

proof

assume A34: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds b . x = FALSE ) ) ; :: thesis: for x being Element of Y holds (a 'or' b) . x = FALSE
let x be Element of Y; :: thesis: (a 'or' b) . x = FALSE
a . x = FALSE by A34;
then (a . x) 'or' (b . x) = FALSE by A34;
hence (a 'or' b) . x = FALSE by Def7; :: thesis: verum

end;

hence ( ( for x being Element of Y holds (a 'or' b) . x = FALSE ) iff ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds b . x = FALSE ) ) ) by A28, A31; :: thesis: verum

end;

then A35: ( ( B_INF a = O_el Y or B_INF b = O_el Y ) & ( B_SUP a = I_el Y or B_SUP b = I_el Y ) ) by A21, A22, Def16, Def17;
then A36: (B_INF a) '&' (B_INF b) = O_el Y by Th8;
(B_SUP a) 'or' (B_SUP b) = I_el Y by A35, Th13;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A21, A36, Def16, Def17; :: thesis: verum

end;

hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A1, A10; :: thesis: verum