set OCL = OpenClosedSetLatt T;

A1: for a, b, c being Element of (OpenClosedSetLatt T) holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)

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 )

( bot "/\" a = bot & a "/\" bot = bot )

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

A1: for a, b, c being Element of (OpenClosedSetLatt T) holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)

proof

reconsider bot = {} T as Element of (OpenClosedSetLatt T) by Th3;
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;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

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

A10:
for a being Element of (OpenClosedSetLatt T) holds
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;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

( bot "/\" a = bot & a "/\" bot = bot )

proof

then A11:
OpenClosedSetLatt T is lower-bounded
;
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;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

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

hence
( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive )
by A1; :: thesis: verum
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;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