let L be with_zero GAD_Lattice; :: thesis: for a being Element of L
for X being set st X = { (x "/\" a) where x is Element of L : verum } holds
( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L )
let a be Element of L; :: thesis: for X being set st X = { (x "/\" a) where x is Element of L : verum } holds
( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L )
let X be set ; :: thesis: ( X = { (x "/\" a) where x is Element of L : verum } implies ( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L ) )
assume B1: X = { (x "/\" a) where x is Element of L : verum } ; :: thesis: ( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L )
B2: for o being object holds
( o in { (x "/\" a) where x is Element of L : verum } iff o in { x where x is Element of L : x [= a } )
proof
let o be object ; :: thesis: ( o in { (x "/\" a) where x is Element of L : verum } iff o in { x where x is Element of L : x [= a } )
hereby :: thesis: ( o in { x where x is Element of L : x [= a } implies o in { (x "/\" a) where x is Element of L : verum } )
assume o in { (x "/\" a) where x is Element of L : verum } ; :: thesis: o in { y where y is Element of L : y [= a }
then consider x being Element of L such that
A1: o = x "/\" a ;
set y = x "/\" a;
L is meet-absorbing ;
then x "/\" a [= a ;
hence o in { y where y is Element of L : y [= a } by A1; :: thesis: verum
end;
assume o in { x where x is Element of L : x [= a } ; :: thesis: o in { (x "/\" a) where x is Element of L : verum }
then consider x being Element of L such that
A1: ( o = x & x [= a ) ;
x "/\" a = x by A1, LATTICES:def 9;
hence o in { (x "/\" a) where x is Element of L : verum } by A1; :: thesis: verum
end;
now :: thesis: for o being object st o in X holds
o in the carrier of L
let o be object ; :: thesis: ( o in X implies o in the carrier of L )
assume o in X ; :: thesis: o in the carrier of L
then consider x being Element of L such that
B3: o = x "/\" a by B1;
thus o in the carrier of L by B3; :: thesis: verum
end;
then reconsider S = X as Subset of L by TARSKI:def 3;
for p, q being Element of L st p in S & q in S holds
p "/\" q in S
proof
let p, q be Element of L; :: thesis: ( p in S & q in S implies p "/\" q in S )
assume p in S ; :: thesis: ( not q in S or p "/\" q in S )
then consider x being Element of L such that
B5: p = x "/\" a by B1;
assume q in S ; :: thesis: p "/\" q in S
then consider y being Element of L such that
B6: q = y "/\" a by B1;
p "/\" q = x "/\" (a "/\" (y "/\" a)) by B5, B6, LATTICES:def 7
.= x "/\" ((a "/\" y) "/\" a) by LATTICES:def 7
.= (x "/\" (a "/\" y)) "/\" a by LATTICES:def 7 ;
hence p "/\" q in S by B1; :: thesis: verum
end;
then B4: S is meet-closed ;
for p, q being Element of L st p in S & q in S holds
p "\/" q in S
proof
let p, q be Element of L; :: thesis: ( p in S & q in S implies p "\/" q in S )
assume p in S ; :: thesis: ( not q in S or p "\/" q in S )
then consider x being Element of L such that
B5: p = x "/\" a by B1;
assume q in S ; :: thesis: p "\/" q in S
then consider y being Element of L such that
B6: q = y "/\" a by B1;
p "\/" q = ((x "/\" a) "\/" y) "/\" ((x "/\" a) "\/" a) by B5, B6, DefLDS
.= ((x "/\" a) "\/" y) "/\" a by LATTICES:def 8 ;
hence p "\/" q in S by B1; :: thesis: verum
end;
then S is join-closed ;
hence ( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L ) by B1, B2, B4, TARSKI:2; :: thesis: verum