let L be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: union Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
now :: thesis: for Y being set st Y in Z holds
Y c= the carrier of L
let Y be set ; :: thesis: ( Y in Z implies Y c= the carrier of L )
assume Y in Z ; :: thesis: Y c= the carrier of L
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= the carrier of L ; :: thesis: verum
end;
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 ; :: according to RELAT_2:def 7 :: thesis: ( 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 ; :: thesis: ( [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 ;
consider bz being set such that
A9: b in bz and
A10: bz in Z by ;
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 ;
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; :: thesis: verum
end;
then reconsider UZ = UZ as Chain of L by ORDERS_2:def 7;
A14: now :: thesis: for Y being set st Y in Z holds
Y c= X `
let Y be set ; :: thesis: ( Y in Z implies Y c= X ` )
assume Y in Z ; :: thesis: 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 ` ; :: thesis: 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 ;
UZ c= X ` by ;
hence union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } by A15; :: thesis: verum
end;
assume x in X ` ; :: thesis: 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 ;
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 :: thesis: 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 ; :: thesis: contradiction
A27: not y in Y by ;
set Y2 = Y \/ {y};
A28: sup Y <= y by ;
the InternalRel of L is_strongly_connected_in Y \/ {y}
proof
let a, b be object ; :: according to RELAT_2:def 7 :: thesis: ( not a in Y \/ {y} or not b in Y \/ {y} or [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
assume A29: ( a in Y \/ {y} & b in Y \/ {y} ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
per cases ( ( a in Y & b in Y ) or ( a in Y & b in {y} ) or ( a in {y} & b in Y ) or ( a in {y} & b in {y} ) ) by ;
suppose A30: ( a in Y & b in Y ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
end;
suppose A31: ( a in Y & b in {y} ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then reconsider a1 = a as Element of L ;
reconsider b1 = b as Element of L by A31;
( b1 = y & a1 <= sup Y ) by ;
then a1 <= b1 by ;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis: verum
end;
suppose A32: ( a in {y} & b in Y ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then reconsider a1 = b as Element of L ;
reconsider b1 = a as Element of L by A32;
( b1 = y & a1 <= sup Y ) by ;
then a1 <= b1 by ;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis: verum
end;
suppose A33: ( a in {y} & b in {y} ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then reconsider a1 = a as Element of L ;
A34: a1 <= a1 ;
( a = y & b = y ) by ;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ; :: thesis: verum
end;
end;
end;
then reconsider Y2 = Y \/ {y} as Chain of L by ORDERS_2:def 7;
{y} c= X ` by ;
then A35: Y2 c= X ` by ;
y in {y} by TARSKI:def 1;
then A36: y in Y2 by XBOOLE_0:def 3;
x in Y2 by ;
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; :: thesis: verum
end;
now :: thesis: not sup Y in X
assume sup Y in X ; :: thesis: contradiction
then consider y being Element of L such that
A37: y in X and
A38: y << sup Y by Def1;
consider d being Element of L such that
A39: d in Y and
A40: y <= d by ;
d in X by ;
hence contradiction by A20, A39, XBOOLE_0:def 5; :: thesis: verum
end;
then sup Y in X ` by XBOOLE_0:def 5;
then sup Y is_maximal_in X ` by ;
hence ex m being Element of L st
( x <= m & m is_maximal_in X ` ) by A22; :: thesis: verum