let L be Lattice; :: thesis: for F being Ideal of L
for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } & a in G holds
G is Ideal of L
let F be Ideal of L; :: thesis: for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } & a in G holds
G is Ideal of L
let a be Element of L; :: thesis: for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } & a in G holds
G is Ideal of L
let G be set ; :: thesis: ( G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } & a in G implies G is Ideal of L )
assume A1: ( G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } & a in G ) ; :: thesis: G is Ideal of L
G c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in G or y in the carrier of L )
assume y in G ; :: thesis: y in the carrier of L
then consider x being Element of L such that
S2: ( y = x & ex u being Element of L st
( u in F & x [= a "\/" u ) ) by A1;
thus y in the carrier of L by S2; :: thesis: verum

end;

then reconsider G = G as Subset of L ;
set u = the Element of F;
ZD: G is join-closed

proof

let p, q be Element of L; :: according to LATTICES:def 25 :: thesis: ( not p in G or not q in G or p "\/" q in G )
assume P0: ( p in G & q in G ) ; :: thesis: p "\/" q in G
then consider xx being Element of L such that
P1: ( xx = p & ex u being Element of L st
( u in F & xx [= a "\/" u ) ) by A1;
consider u1 being Element of L such that
P3: ( u1 in F & p [= a "\/" u1 ) by P1;
consider yy being Element of L such that
P2: ( yy = q & ex u being Element of L st
( u in F & yy [= a "\/" u ) ) by P0, A1;
consider u2 being Element of L such that
P4: ( u2 in F & q [= a "\/" u2 ) by P2;
P6: p "\/" q [= (a "\/" u1) "\/" (a "\/" u2) by P3, P4, FILTER_0:4;
P7: u1 "\/" u2 in F by P3, P4, FILTER_2:86;
(a "\/" u1) "\/" (a "\/" u2) = ((a "\/" u1) "\/" a) "\/" u2 by LATTICES:def 5
.= ((a "\/" a) "\/" u1) "\/" u2 by LATTICES:def 5
.= a "\/" (u1 "\/" u2) by LATTICES:def 5 ;
hence p "\/" q in G by P7, P6, A1; :: thesis: verum

end;

G is initial

proof

let p, q be Element of L; :: according to LATTICES:def 22 :: thesis: ( not p [= q or not q in G or p in G )
assume Y0: ( p [= q & q in G ) ; :: thesis: p in G
then consider s being Element of L such that
Y1: ( s = q & ex u being Element of L st
( u in F & s [= a "\/" u ) ) by A1;
consider u being Element of L such that
Y2: ( u in F & s [= a "\/" u ) by Y1;
p [= a "\/" u by Y2, Y0, Y1, LATTICES:7;
hence p in G by Y2, A1; :: thesis: verum

end;

hence G is Ideal of L by ZD, A1; :: thesis: verum