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;
( a in F or b in F ) by A3, A4;
then ( F in (StoneH L) . a or F in (StoneH L) . b ) by A2, A3, Th12;
hence x in ((StoneH L) . a) \/ ((StoneH L) . b) by A1, XBOOLE_0:def 3; :: 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 x in ((StoneH L) . a) \/ ((StoneH L) . b) ; :: thesis: x in (StoneH L) . (a "\/" b)
then ( x in (StoneH L) . a or x in (StoneH L) . b ) by XBOOLE_0:def 3;
then ( ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & a in F ) or ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & b in F ) ) by Th12;
then consider F being Filter of L such that
A5: x = F and
A6: F <> the carrier of L and
A7: F is prime and
A8: ( a in F or b in F ) ;
a "\/" b in F by A7, A8;
hence x in (StoneH L) . (a "\/" b) by A5, A6, A7, Th12; :: thesis: verum