let L be with_zero GAD_Lattice; :: thesis: for a being Element of L
for S being non empty ClosedSubset of L
for b being Element of (latt (L,S)) st b = a & S = { (x "/\" a) where x is Element of L : verum } holds
( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) )
let a be Element of L; :: thesis: for S being non empty ClosedSubset of L
for b being Element of (latt (L,S)) st b = a & S = { (x "/\" a) where x is Element of L : verum } holds
( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) )
let S be non empty ClosedSubset of L; :: thesis: for b being Element of (latt (L,S)) st b = a & S = { (x "/\" a) where x is Element of L : verum } holds
( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) )
let b be Element of (latt (L,S)); :: thesis: ( b = a & S = { (x "/\" a) where x is Element of L : verum } implies ( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) ) )
assume Z5: b = a ; :: thesis: ( not S = { (x "/\" a) where x is Element of L : verum } or ( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) ) )
assume Z2: S = { (x "/\" a) where x is Element of L : verum } ; :: thesis: ( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) )
for y1, y2 being Element of (latt (L,S)) holds y1 "/\" y2 = y2 "/\" y1
proof
let y1, y2 be Element of (latt (L,S)); :: thesis: y1 "/\" y2 = y2 "/\" y1
y1 in the carrier of (latt (L,S)) ;
then y1 in S by Defx4;
then consider x1 being Element of L such that
B1: y1 = x1 "/\" a by Z2;
y2 in the carrier of (latt (L,S)) ;
then y2 in S by Defx4;
then consider x2 being Element of L such that
B2: y2 = x2 "/\" a by Z2;
thus y1 "/\" y2 = (x1 "/\" a) "/\" (x2 "/\" a) by B1, B2, Thx4
.= (a "/\" x1) "/\" (x2 "/\" a) by Lem310
.= a "/\" (x1 "/\" (x2 "/\" a)) by LATTICES:def 7
.= a "/\" ((x1 "/\" x2) "/\" a) by LATTICES:def 7
.= a "/\" ((x2 "/\" x1) "/\" a) by Lem310
.= a "/\" (x2 "/\" (x1 "/\" a)) by LATTICES:def 7
.= (a "/\" x2) "/\" (x1 "/\" a) by LATTICES:def 7
.= (x2 "/\" a) "/\" (x1 "/\" a) by Lem310
.= y2 "/\" y1 by B1, B2, Thx4 ; :: thesis: verum
end;
then Z12: latt (L,S) is meet-commutative ;
latt (L,S) is GAD_Lattice by Thx1;
hence ( latt (L,S) is Lattice-like & latt (L,S) is distributive ) by Z12, Th31141; :: thesis: for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b )
let c be Element of (latt (L,S)); :: thesis: ( b "\/" c = b & c "\/" b = b & c [= b )
c in the carrier of (latt (L,S)) ;
then c in S by Defx4;
then consider x being Element of L such that
A1: c = x "/\" a by Z2;
reconsider d = c as Element of L by A1;
thus b "\/" c = a "\/" (x "/\" a) by A1, Z5, Thx3
.= b by Z5, ThA5 ; :: thesis: ( c "\/" b = b & c [= b )
thus A2: c "\/" b = (x "/\" a) "\/" a by A1, Z5, Thx3
.= b by Z5, LATTICES:def 8 ; :: thesis: c [= b
thus c [= b by A2; :: thesis: verum