let K be Lattice; ( K is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) )
thus
( K is SubLattice of L implies ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) )
( ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) implies K is Sublattice of L )proof
assume A1:
K is
SubLattice of
L
;
ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
then A2:
H3(
K)
= H3(
L)
|| H1(
K)
by NAT_LAT:def 12;
reconsider P =
H1(
K) as non
empty Subset of
L by A1, NAT_LAT:def 12;
A3:
H2(
K)
= H2(
L)
|| H1(
K)
by A1, NAT_LAT:def 12;
now for p, q being Element of L st p in P & q in P holds
( p "/\" q in P & p "\/" q in P )let p,
q be
Element of
L;
( p in P & q in P implies ( p "/\" q in P & p "\/" q in P ) )assume
(
p in P &
q in P )
;
( p "/\" q in P & p "\/" q in P )then A4:
[p,q] in [:P,P:]
by ZFMISC_1:87;
dom H3(
K)
= [:P,P:]
by FUNCT_2:def 1;
then A5:
H3(
L)
. [p,q] = H3(
K)
. [p,q]
by A2, A4, FUNCT_1:47;
dom H2(
K)
= [:P,P:]
by FUNCT_2:def 1;
then
H2(
L)
. [p,q] = H2(
K)
. [p,q]
by A3, A4, FUNCT_1:47;
hence
(
p "/\" q in P &
p "\/" q in P )
by A4, A5, FUNCT_2:5;
verum end;
then
( ( for
p1,
p2 being
Element of
L st
p1 in P &
p2 in P holds
p1 "/\" p2 in P ) & ( for
p1,
p2 being
Element of
L st
p1 in P &
p2 in P holds
p1 "\/" p2 in P ) )
;
then reconsider P =
P as non
empty ClosedSubset of
L by LATTICES:def 24, LATTICES:def 25;
take
P
;
ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
reconsider o1 =
H2(
K),
o2 =
H3(
K) as
BinOp of
P ;
take
o1
;
ex o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
take
o2
;
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
thus
(
o1 = the
L_join of
L || P &
o2 = the
L_meet of
L || P &
LattStr(# the
carrier of
K, the
L_join of
K, the
L_meet of
K #)
= LattStr(#
P,
o1,
o2 #) )
by A1, NAT_LAT:def 12;
verum
end;
given P being non empty ClosedSubset of L, o1, o2 being BinOp of P such that A6:
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
; K is Sublattice of L
thus
K is Sublattice of L
by A6, NAT_LAT:def 12; verum