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

proof

let a be Element of (OpenClosedSetLatt T); :: thesis: ( top "\/" a = top & a "\/" top = top )
reconsider a9 = a as Element of OpenClosedSet T ;
thus top "\/" a = ([#] T) \/ a9 by Def2
.= top by XBOOLE_1:12 ; :: thesis: a "\/" top = top
hence a "\/" top = top ; :: thesis: verum

end;

A10: for a being Element of (OpenClosedSetLatt T) holds
( bot "/\" a = bot & a "/\" bot = bot )

proof

let a be Element of (OpenClosedSetLatt T); :: thesis: ( bot "/\" a = bot & a "/\" bot = bot )
reconsider a9 = a as Element of OpenClosedSet T ;
thus bot "/\" a = {} /\ a9 by Def3
.= bot ; :: thesis: a "/\" bot = bot
hence a "/\" bot = bot ; :: thesis: verum

end;

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; :: according to LATTICES:def 20 :: thesis: ( 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

proof

let b be Element of OCL; :: thesis: ex a being Element of OCL st a is_a_complement_of b
reconsider c = b as Element of OpenClosedSet T ;
reconsider a = c ` as Element of OCL by Th8;
A15: a "\/" b = c \/ (c `) by Def2
.= Top OCL by A14, PRE_TOPC:2 ;
A16: c misses c ` by XBOOLE_1:79;
A17: a "/\" b = c /\ (c `) by Def3
.= Bottom OCL by A13, A16 ;
take a ; :: thesis: a is_a_complement_of b
( a "\/" b = b "\/" a & a "/\" b = b "/\" a ) ;
hence a is_a_complement_of b by A15, A17; :: thesis: verum

end;

hence ( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive ) by A1; :: thesis: verum