set OCL = OpenClosedSetLatt T;
A1: for a, b, c being Element of holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
proof
let a, b, c be Element of ; :: 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 by Th3;
reconsider top = [#] T as Element of by Th3;
A9: for a being Element of holds
( top "\/" a = top & a "\/" top = top )
proof
let a be Element of ; :: 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 holds
( bot "/\" a = bot & a "/\" bot = bot )
proof
let a be Element of ; :: 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 by ;
A14: [#] T = Top by ;
thus OpenClosedSetLatt T is bounded by ; :: according to LATTICES:def 20 :: thesis:
reconsider OCL = OpenClosedSetLatt T as 01_Lattice by ;
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 ;
A16: c misses c ` by XBOOLE_1:79;
A17: a "/\" b = c /\ (c `) by Def3
.= Bottom OCL by ;
take a ; :: thesis:
( a "\/" b = b "\/" a & a "/\" b = b "/\" a ) ;
hence a is_a_complement_of b by ; :: thesis: verum
end;
hence ( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive ) by A1; :: thesis: verum