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

hence LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice ; :: thesis: verum

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;thus p "\/" q = q \/ p by Def9

.= q "\/" p by Def9 ; :: thesis: verum

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;thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def9

.= (p /\ q) \/ q by Def10

.= q by XBOOLE_1:22 ; :: thesis: verum

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;thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def10

.= p /\ (p \/ q) by Def9

.= p by XBOOLE_1:21 ; :: thesis: verum

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

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;thus p "/\" q = q /\ p by Def10

.= q "/\" p by Def10 ; :: thesis: verum

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

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

hence LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice ; :: thesis: verum