let L be WA-Lattice; ( the InternalRel of L is transitive implies wlatt L is Lattice )
A1:
field the InternalRel of L = the carrier of L
by ORDERS_1:12;
assume
the InternalRel of L is transitive
; wlatt L is Lattice
then
the InternalRel of L is_transitive_in field the InternalRel of L
by RELAT_2:def 16;
then reconsider LL = L as with_suprema with_infima Poset by ORDERS_2:def 3, A1;
B1:
RelStr(# the carrier of LL, the InternalRel of LL #) = LatRelStr (wlatt LL)
by WLatDef;
BC:
RelStr(# the carrier of LL, the InternalRel of LL #) = LattPOSet (latt LL)
by LATTICE3:def 15;
then BB:
LatRelStr (wlatt LL) = LattPOSet (latt LL)
by B1;
set L1 = latt LL;
set L2 = wlatt LL;
D2:
the carrier of (latt LL) = the carrier of (wlatt LL)
by BB;
LatOrder (latt LL) = LatOrder (wlatt LL)
proof
T1:
LatOrder (latt LL) c= LatOrder (wlatt LL)
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in LatOrder (latt LL) or [x,y] in LatOrder (wlatt LL) )
assume
[x,y] in LatOrder (latt LL)
;
[x,y] in LatOrder (wlatt LL)
then consider a,
b being
Element of
(latt LL) such that A1:
(
[x,y] = [a,b] &
a [= b )
;
reconsider aa =
a,
bb =
b as
Element of
(wlatt LL) by D2;
reconsider a1 =
a,
b1 =
b as
Element of
L by BC;
a1 <= b1
by A1, Eq1;
then
(
[aa,bb] = [x,y] &
aa [= bb )
by A1, Eq2;
hence
[x,y] in LatOrder (wlatt LL)
;
verum
end;
LatOrder (wlatt LL) c= LatOrder (latt LL)
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in LatOrder (wlatt LL) or [x,y] in LatOrder (latt LL) )
assume
[x,y] in LatOrder (wlatt LL)
;
[x,y] in LatOrder (latt LL)
then consider a,
b being
Element of
(wlatt LL) such that A1:
(
[x,y] = [a,b] &
a [= b )
;
reconsider aa =
a,
bb =
b as
Element of
(latt LL) by D2;
reconsider a1 =
a,
b1 =
b as
Element of
L by B1;
a1 <= b1
by A1, Eq2;
then
(
[aa,bb] = [x,y] &
aa [= bb )
by A1, Eq1;
hence
[x,y] in LatOrder (latt LL)
;
verum
end;
hence
LatOrder (latt LL) = LatOrder (wlatt LL)
by T1, XBOOLE_0:def 10;
verum
end;
then
LatRelStr (latt LL) = LatRelStr (wlatt LL)
by D2;
hence
wlatt L is Lattice
by Th6; verum