let L be D_Lattice; :: thesis: for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
let a, b be Element of L; :: thesis: (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
set c = a "/\" b;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ((StoneH L) . a) /\ ((StoneH L) . b) c= (StoneH L) . (a "/\" b)

set c = a "/\" b;
let x be object ; :: thesis: ( x in (StoneH L) . (a "/\" b) implies x in ((StoneH L) . a) /\ ((StoneH L) . b) )
assume x in (StoneH L) . (a "/\" b) ; :: thesis: x in ((StoneH L) . a) /\ ((StoneH L) . 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 A4, FILTER_0:8;
then A5: F in (StoneH L) . b by A2, A3, Th12;
a in F by A4, FILTER_0:8;
then F in (StoneH L) . a by A2, A3, Th12;
hence x in ((StoneH L) . a) /\ ((StoneH L) . b) by A1, A5, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((StoneH L) . a) /\ ((StoneH L) . b) or x in (StoneH L) . (a "/\" b) )
assume A6: x in ((StoneH L) . a) /\ ((StoneH L) . b) ; :: thesis: x in (StoneH L) . (a "/\" b)
then x in (StoneH L) . 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 (StoneH L) . a by A6, XBOOLE_0:def 4;
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 A11, A12, FILTER_0:8;
hence x in (StoneH L) . (a "/\" b) by A8, A9, A10, Th12; :: thesis: verum