let C be FormalContext; ConceptLattice C is Lattice
set L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);
reconsider L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) as non empty strict LattStr ;
A1:
for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a,
b,
c be
Element of
L;
a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider b =
b,
c =
c as
Element of
B-carrier C ;
reconsider d =
(B-join C) . (
b,
c) as
Element of
L ;
reconsider b =
b,
c =
c as
Element of
L ;
reconsider a =
a,
b =
b as
Element of
B-carrier C ;
reconsider e =
(B-join C) . (
a,
b) as
Element of
L ;
reconsider a =
a,
b =
b as
Element of
L ;
A2:
a "\/" (b "\/" c) =
a "\/" d
by LATTICES:def 1
.=
(B-join C) . (
a,
((B-join C) . (b,c)))
by LATTICES:def 1
;
A3:
(a "\/" b) "\/" c =
e "\/" c
by LATTICES:def 1
.=
(B-join C) . (
((B-join C) . (a,b)),
c)
by LATTICES:def 1
;
reconsider a =
a,
b =
b,
c =
c as
strict FormalConcept of
C by Th31;
(B-join C) . (
a,
((B-join C) . (b,c)))
= (B-join C) . (
((B-join C) . (a,b)),
c)
by Th35;
hence
a "\/" (b "\/" c) = (a "\/" b) "\/" c
by A2, A3;
verum
end;
A4:
for a, b being Element of L holds (a "/\" b) "\/" b = b
A6:
for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a,
b,
c be
Element of
L;
a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider b =
b,
c =
c as
Element of
B-carrier C ;
reconsider d =
(B-meet C) . (
b,
c) as
Element of
L ;
reconsider b =
b,
c =
c as
Element of
L ;
A7:
a "/\" (b "/\" c) =
a "/\" d
by LATTICES:def 2
.=
(B-meet C) . (
a,
((B-meet C) . (b,c)))
by LATTICES:def 2
;
reconsider a =
a,
b =
b as
Element of
B-carrier C ;
reconsider e =
(B-meet C) . (
a,
b) as
Element of
L ;
reconsider a =
a,
b =
b as
Element of
L ;
A8:
(a "/\" b) "/\" c =
e "/\" c
by LATTICES:def 2
.=
(B-meet C) . (
((B-meet C) . (a,b)),
c)
by LATTICES:def 2
;
reconsider a =
a,
b =
b,
c =
c as
strict FormalConcept of
C by Th31;
(B-meet C) . (
a,
((B-meet C) . (b,c)))
= (B-meet C) . (
((B-meet C) . (a,b)),
c)
by Th34;
hence
a "/\" (b "/\" c) = (a "/\" b) "/\" c
by A7, A8;
verum
end;
A9:
for a, b being Element of L holds a "/\" b = b "/\" a
A11:
for a, b being Element of L holds a "/\" (a "\/" b) = a
for a, b being Element of L holds a "\/" b = b "\/" a
then
( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
by A1, A4, A9, A6, A11, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence
ConceptLattice C is Lattice
; verum