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;

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

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)

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) )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 ; :: 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

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