let L be complete LATTICE; for X being upper Open Subset of L
for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
let X be upper Open Subset of L; for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
let x be Element of L; ( x in X ` implies ex m being Element of L st
( x <= m & m is_maximal_in X ` ) )
set A = { C where C is Chain of L : ( C c= X ` & x in C ) } ;
reconsider x1 = {x} as Chain of L by ORDERS_2:8;
A1:
for Z being set st Z <> {} & Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } & Z is c=-linear holds
union Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
proof
let Z be
set ;
( Z <> {} & Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } & Z is c=-linear implies union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } )
assume that A2:
Z <> {}
and A3:
Z c= { C where C is Chain of L : ( C c= X ` & x in C ) }
and A4:
Z is
c=-linear
;
union Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
then reconsider UZ =
union Z as
Subset of
L by ZFMISC_1:76;
the
InternalRel of
L is_strongly_connected_in UZ
proof
let a,
b be
object ;
RELAT_2:def 7 ( not a in UZ or not b in UZ or [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
assume that A5:
a in UZ
and A6:
b in UZ
;
( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
consider az being
set such that A7:
a in az
and A8:
az in Z
by A5, TARSKI:def 4;
consider bz being
set such that A9:
b in bz
and A10:
bz in Z
by A6, TARSKI:def 4;
az,
bz are_c=-comparable
by A4, A8, A10;
then A11:
(
az c= bz or
bz c= az )
;
bz in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A3, A10;
then A12:
ex
C being
Chain of
L st
(
bz = C &
C c= X ` &
x in C )
;
az in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A3, A8;
then A13:
ex
C being
Chain of
L st
(
az = C &
C c= X ` &
x in C )
;
reconsider bz =
bz as
Chain of
L by A12;
reconsider az =
az as
Chain of
L by A13;
( the
InternalRel of
L is_strongly_connected_in az & the
InternalRel of
L is_strongly_connected_in bz )
by ORDERS_2:def 7;
hence
(
[a,b] in the
InternalRel of
L or
[b,a] in the
InternalRel of
L )
by A7, A9, A11;
verum
end;
then reconsider UZ =
UZ as
Chain of
L by ORDERS_2:def 7;
A14:
now for Y being set st Y in Z holds
Y c= X ` let Y be
set ;
( Y in Z implies Y c= X ` )assume
Y in Z
;
Y c= X ` then
Y in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A3;
then
ex
C being
Chain of
L st
(
Y = C &
C c= X ` &
x in C )
;
hence
Y c= X `
;
verum end;
set Y = the
Element of
Z;
the
Element of
Z in Z
by A2;
then
the
Element of
Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A3;
then
ex
C being
Chain of
L st
( the
Element of
Z = C &
C c= X ` &
x in C )
;
then A15:
x in UZ
by A2, TARSKI:def 4;
UZ c= X `
by A14, ZFMISC_1:76;
hence
union Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A15;
verum
end;
assume
x in X `
; ex m being Element of L st
( x <= m & m is_maximal_in X ` )
then A16:
x1 c= X `
by ZFMISC_1:31;
x in x1
by ZFMISC_1:31;
then
x1 in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A16;
then consider Y1 being set such that
A17:
Y1 in { C where C is Chain of L : ( C c= X ` & x in C ) }
and
A18:
for Z being set st Z in { C where C is Chain of L : ( C c= X ` & x in C ) } & Z <> Y1 holds
not Y1 c= Z
by A1, ORDERS_1:67;
consider Y being Chain of L such that
A19:
Y = Y1
and
A20:
Y c= X `
and
A21:
x in Y
by A17;
set m = sup Y;
sup Y is_>=_than Y
by YELLOW_0:32;
then A22:
x <= sup Y
by A21;
A23:
sup Y is_>=_than Y
by YELLOW_0:32;
A24:
now for y being Element of L holds
( not y in X ` or not y > sup Y )given y being
Element of
L such that A25:
y in X `
and A26:
y > sup Y
;
contradictionA27:
not
y in Y
by A26, ORDERS_2:6, A23;
set Y2 =
Y \/ {y};
A28:
sup Y <= y
by A26, ORDERS_2:def 6;
the
InternalRel of
L is_strongly_connected_in Y \/ {y}
then reconsider Y2 =
Y \/ {y} as
Chain of
L by ORDERS_2:def 7;
{y} c= X `
by A25, ZFMISC_1:31;
then A35:
Y2 c= X `
by A20, XBOOLE_1:8;
y in {y}
by TARSKI:def 1;
then A36:
y in Y2
by XBOOLE_0:def 3;
x in Y2
by A21, XBOOLE_0:def 3;
then
Y2 in { C where C is Chain of L : ( C c= X ` & x in C ) }
by A35;
hence
contradiction
by A18, A19, A27, A36, XBOOLE_1:7;
verum end;
then
sup Y in X `
by XBOOLE_0:def 5;
then
sup Y is_maximal_in X `
by A24, WAYBEL_4:55;
hence
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
by A22; verum