let Y be non empty set ; :: thesis:
let a, b be Function of Y,BOOLEAN; :: thesis:

A1: now :: thesis:

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

proof

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

end;

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

proof

now :: thesis:

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

end;

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

end;

then A4: B_SUP a = I_el Y by Def14;
A5: for x being Element of Y holds b . x = TRUE

proof

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

end;

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

proof

now :: thesis:

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

end;

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

end;

then A6: (B_SUP a) 'or' (B_SUP b) = (I_el Y) 'or' (I_el Y) by A4, Def14;
A7: not for x being Element of Y holds (a 'or' b) . x = FALSE

proof

now :: thesis:

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

end;

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

end;

(B_INF a) '&' (B_INF b) = (B_INF a) '&' (I_el Y) by A5, Def13
.= (I_el Y) '&' (I_el Y) by A3, Def13 ;
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, A7, A6, Def13, Def14; :: thesis:

end;

A8: now :: thesis:

assume A9: for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis:
A10: for x being Element of Y holds a . x = FALSE

proof

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

end;

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

proof

now :: thesis:

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

end;

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

end;

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

proof

let x be Element of Y; :: thesis:
(a 'or' b) . x = FALSE by A9;
then A14: (a . x) 'or' (b . x) = FALSE by Def4;
( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def 3;
hence b . x = FALSE by A14; :: thesis:

end;

then B_SUP b = O_el Y by Def14;
then A15: (B_SUP a) 'or' (B_SUP b) = (O_el Y) 'or' (O_el Y) by A10, Def14;
not for x being Element of Y holds a . x = TRUE

proof

now :: thesis:

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

end;

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

end;

then A16: B_INF a = O_el Y by Def13;
not for x being Element of Y holds b . x = TRUE

proof

now :: thesis:

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

end;

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

end;

then (B_INF a) '&' (B_INF b) = (O_el Y) '&' (O_el Y) by A16, Def13;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A9, A15, A12, Def13, Def14; :: thesis:

end;

now :: thesis:

assume that
A17: not for x being Element of Y holds (a '&' b) . x = TRUE and
A18: not for x being Element of Y holds (a 'or' b) . x = FALSE ; :: thesis:
( ( 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 that
A19: for x being Element of Y holds a . x = FALSE and
A20: for x being Element of Y holds b . x = FALSE ; :: thesis:
let x be Element of Y; :: thesis:
a . x = FALSE by A19;
then (a . x) 'or' (b . x) = FALSE by A20;
hence (a 'or' b) . x = FALSE by Def4; :: thesis:

end;

then ( B_SUP a = I_el Y or B_SUP b = I_el Y ) by A18, Def14;
then A21: (B_SUP a) 'or' (B_SUP b) = I_el Y by Th9;
( ( 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 that
A22: for x being Element of Y holds a . x = TRUE and
A23: for x being Element of Y holds b . x = TRUE ; :: thesis:
let x be Element of Y; :: thesis:
a . x = TRUE by A22;
then (a . x) '&' (b . x) = TRUE by A23;
hence (a '&' b) . x = TRUE by MARGREL1:def 20; :: thesis:

end;

then ( B_INF a = O_el Y or B_INF b = O_el Y ) by A17, Def13;
then (B_INF a) '&' (B_INF b) = O_el Y by Th4;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A17, A18, A21, Def13, Def14; :: thesis:

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, A8; :: thesis: