let BL be non trivial B_Lattice; :: thesis: for a, b being Element of BL holds (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)

let a, b be Element of BL; :: thesis: (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)

A1: (UFilter BL) . (a "/\" b) c= ((UFilter BL) . a) /\ ((UFilter BL) . b)

let a, b be Element of BL; :: thesis: (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)

A1: (UFilter BL) . (a "/\" b) c= ((UFilter BL) . a) /\ ((UFilter BL) . b)

proof

((UFilter BL) . a) /\ ((UFilter BL) . b) c= (UFilter BL) . (a "/\" b)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UFilter BL) . (a "/\" b) or x in ((UFilter BL) . a) /\ ((UFilter BL) . b) )

set c = a "/\" b;

assume x in (UFilter BL) . (a "/\" b) ; :: thesis: x in ((UFilter BL) . a) /\ ((UFilter BL) . b)

then consider F0 being Filter of BL such that

A2: x = F0 and

A3: F0 is being_ultrafilter and

A4: a "/\" b in F0 by Th17;

A5: a in F0 by A4, FILTER_0:8;

A6: b in F0 by A4, FILTER_0:8;

A7: F0 in (UFilter BL) . a by A3, A5, Th17;

F0 in (UFilter BL) . b by A3, A6, Th17;

hence x in ((UFilter BL) . a) /\ ((UFilter BL) . b) by A2, A7, XBOOLE_0:def 4; :: thesis: verum

end;set c = a "/\" b;

assume x in (UFilter BL) . (a "/\" b) ; :: thesis: x in ((UFilter BL) . a) /\ ((UFilter BL) . b)

then consider F0 being Filter of BL such that

A2: x = F0 and

A3: F0 is being_ultrafilter and

A4: a "/\" b in F0 by Th17;

A5: a in F0 by A4, FILTER_0:8;

A6: b in F0 by A4, FILTER_0:8;

A7: F0 in (UFilter BL) . a by A3, A5, Th17;

F0 in (UFilter BL) . b by A3, A6, Th17;

hence x in ((UFilter BL) . a) /\ ((UFilter BL) . b) by A2, A7, XBOOLE_0:def 4; :: thesis: verum

proof

hence
(UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((UFilter BL) . a) /\ ((UFilter BL) . b) or x in (UFilter BL) . (a "/\" b) )

assume A8: x in ((UFilter BL) . a) /\ ((UFilter BL) . b) ; :: thesis: x in (UFilter BL) . (a "/\" b)

then A9: x in (UFilter BL) . a by XBOOLE_0:def 4;

A10: x in (UFilter BL) . b by A8, XBOOLE_0:def 4;

A11: ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & a in F0 ) by A9, Th17;

ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & b in F0 ) by A10, Th17;

then consider F0 being Filter of BL such that

A12: x = F0 and

A13: F0 is being_ultrafilter and

A14: a in F0 and

A15: b in F0 by A11;

a "/\" b in F0 by A14, A15, FILTER_0:8;

hence x in (UFilter BL) . (a "/\" b) by A12, A13, Th17; :: thesis: verum

end;assume A8: x in ((UFilter BL) . a) /\ ((UFilter BL) . b) ; :: thesis: x in (UFilter BL) . (a "/\" b)

then A9: x in (UFilter BL) . a by XBOOLE_0:def 4;

A10: x in (UFilter BL) . b by A8, XBOOLE_0:def 4;

A11: ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & a in F0 ) by A9, Th17;

ex F0 being Filter of BL st

( x = F0 & F0 is being_ultrafilter & b in F0 ) by A10, Th17;

then consider F0 being Filter of BL such that

A12: x = F0 and

A13: F0 is being_ultrafilter and

A14: a in F0 and

A15: b in F0 by A11;

a "/\" b in F0 by A14, A15, FILTER_0:8;

hence x in (UFilter BL) . (a "/\" b) by A12, A13, Th17; :: thesis: verum