let L be D_Lattice; :: thesis: for a, b being Element of L holds () . (a "/\" b) = (() . a) /\ (() . b)
let a, b be Element of L; :: thesis: () . (a "/\" b) = (() . a) /\ (() . b)
set c = a "/\" b;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (() . a) /\ (() . b) c= () . (a "/\" b)
set c = a "/\" b;
let x be object ; :: thesis: ( x in () . (a "/\" b) implies x in (() . a) /\ (() . b) )
assume x in () . (a "/\" b) ; :: thesis: x in (() . a) /\ (() . b)
then consider F being Filter of L such that
A1: x = F and
A2: F <> the carrier of L and
A3: F is prime and
A4: a "/\" b in F by Th12;
b in F by ;
then A5: F in () . b by A2, A3, Th12;
a in F by ;
then F in () . a by A2, A3, Th12;
hence x in (() . a) /\ (() . b) by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (() . a) /\ (() . b) or x in () . (a "/\" b) )
assume A6: x in (() . a) /\ (() . b) ; :: thesis: x in () . (a "/\" b)
then x in () . b by XBOOLE_0:def 4;
then A7: ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & b in F ) by Th12;
x in () . a by ;
then ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & a in F ) by Th12;
then consider F being Filter of L such that
A8: x = F and
A9: F <> the carrier of L and
A10: F is prime and
A11: a in F and
A12: b in F by A7;
a "/\" b in F by ;
hence x in () . (a "/\" b) by A8, A9, A10, Th12; :: thesis: verum