let L be D_Lattice; :: thesis: LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice
set SL = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);

A1: now :: thesis: for p, q being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds p "\/" q = q "\/" p

let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); :: thesis: p "\/" q = q "\/" p
thus p "\/" q = q \/ p by Def9
.= q "\/" p by Def9 ; :: thesis: verum

end;

A2: now :: thesis: for p, q being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds (p "/\" q) "\/" q = q

let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); :: thesis: (p "/\" q) "\/" q = q
thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def9
.= (p /\ q) \/ q by Def10
.= q by XBOOLE_1:22 ; :: thesis: verum

end;

A3: now :: thesis: for p, q being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds p "/\" (p "\/" q) = p

let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); :: thesis: p "/\" (p "\/" q) = p
thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def10
.= p /\ (p \/ q) by Def9
.= p by XBOOLE_1:21 ; :: thesis: verum

end;

A4: now :: thesis: for p, q, r being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds p "/\" (q "/\" r) = (p "/\" q) "/\" r

let p, q, r be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
thus p "/\" (q "/\" r) = p /\ (q "/\" r) by Def10
.= p /\ (q /\ r) by Def10
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def10
.= (p "/\" q) "/\" r by Def10 ; :: thesis: verum

end;

A5: now :: thesis: for p, q being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds p "/\" q = q "/\" p

let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); :: thesis: p "/\" q = q "/\" p
thus p "/\" q = q /\ p by Def10
.= q "/\" p by Def10 ; :: thesis: verum

end;

now :: thesis: for p, q, r being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds p "\/" (q "\/" r) = (p "\/" q) "\/" r

let p, q, r be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
thus p "\/" (q "\/" r) = p \/ (q "\/" r) by Def9
.= p \/ (q \/ r) by Def9
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def9
.= (p "\/" q) "\/" r by Def9 ; :: thesis: verum

end;

then ( LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-commutative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-associative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-absorbing & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-commutative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-associative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-absorbing ) by A1, A2, A5, A4, A3;
hence LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice ; :: thesis: verum