let L be lower-bounded up-complete LATTICE; for X being Subset of L holds
( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
let X be Subset of L; ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
thus
( X is order-generating implies for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y ) implies X is order-generating )
thus
( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y ) implies X is order-generating )
verumproof
set Y =
{ ("/\" (Z,L)) where Z is Subset of L : Z c= X } ;
then reconsider Y =
{ ("/\" (Z,L)) where Z is Subset of L : Z c= X } as
Subset of
L by TARSKI:def 3;
then A7:
X c= Y
;
assume A8:
for
Y being
Subset of
L st
X c= Y & ( for
Z being
Subset of
Y holds
"/\" (
Z,
L)
in Y ) holds
the
carrier of
L = Y
;
X is order-generating
for
l being
Element of
L ex
Z being
Subset of
X st
l = "/\" (
Z,
L)
proof
let l be
Element of
L;
ex Z being Subset of X st l = "/\" (Z,L)
for
Z being
Subset of
Y holds
"/\" (
Z,
L)
in Y
proof
let Z be
Subset of
Y;
"/\" (Z,L) in Y
set S =
union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ;
then reconsider S =
union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } as
Subset of
L by TARSKI:def 3;
defpred S1[
Subset of
L]
means ( $1
c= X &
"/\" ($1,
L)
in Z );
set N =
{ ("/\" (A,L)) where A is Subset of L : S1[A] } ;
then A12:
Z c= { ("/\" (A,L)) where A is Subset of L : S1[A] }
;
then A13:
S c= X
by ZFMISC_1:76;
then
{ ("/\" (A,L)) where A is Subset of L : S1[A] } c= Z
;
then "/\" (
Z,
L) =
"/\" (
{ ("/\" (A,L)) where A is Subset of L : S1[A] } ,
L)
by A12, XBOOLE_0:def 10
.=
"/\" (
(union { A where A is Subset of L : S1[A] } ),
L)
from YELLOW_3:sch 3()
;
hence
"/\" (
Z,
L)
in Y
by A13;
verum
end;
then
the
carrier of
L = Y
by A8, A7;
then
l in Y
;
then
ex
Z being
Subset of
L st
(
l = "/\" (
Z,
L) &
Z c= X )
;
hence
ex
Z being
Subset of
X st
l = "/\" (
Z,
L)
;
verum
end;
hence
X is
order-generating
by Th15;
verum
end;