set OCL = OpenClosedSetLatt T;
A1:
for a, b, c being Element of (OpenClosedSetLatt T) holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
proof
let a,
b,
c be
Element of
(OpenClosedSetLatt T);
a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
set m =
a "/\" c;
consider a9,
b9,
c9,
k9,
l9,
m9 being
Element of
OpenClosedSet T such that A2:
a = a9
and A3:
b = b9
and A4:
c = c9
and A5:
b "\/" c = k9
and A6:
a "/\" b = l9
and A7:
a "/\" c = m9
;
A8:
a9 /\ c9 = a "/\" c
by A2, A4, Def3;
thus a "/\" (b "\/" c) =
a9 /\ k9
by A2, A5, Def3
.=
a9 /\ (b9 \/ c9)
by A3, A4, A5, Def2
.=
(a9 /\ b9) \/ (a9 /\ c9)
by XBOOLE_1:23
.=
l9 \/ m9
by A2, A3, A6, A7, A8, Def3
.=
(a "/\" b) "\/" (a "/\" c)
by A6, A7, Def2
;
verum
end;
reconsider bot = {} T as Element of (OpenClosedSetLatt T) by Th3;
reconsider top = [#] T as Element of (OpenClosedSetLatt T) by Th3;
A9:
for a being Element of (OpenClosedSetLatt T) holds
( top "\/" a = top & a "\/" top = top )
A10:
for a being Element of (OpenClosedSetLatt T) holds
( bot "/\" a = bot & a "/\" bot = bot )
then A11:
OpenClosedSetLatt T is lower-bounded
;
A12:
OpenClosedSetLatt T is upper-bounded
by A9;
A13:
{} T = Bottom (OpenClosedSetLatt T)
by A10, A11, LATTICES:def 16;
A14:
[#] T = Top (OpenClosedSetLatt T)
by A9, A12, LATTICES:def 17;
thus
OpenClosedSetLatt T is bounded
by A11, A12; LATTICES:def 20 ( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive )
reconsider OCL = OpenClosedSetLatt T as 01_Lattice by A11, A12;
for b being Element of OCL ex a being Element of OCL st a is_a_complement_of b
hence
( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive )
by A1; verum