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)

proof

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;

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

proof

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;

hence (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b) by A1; :: thesis: verum