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 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; :: 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 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; :: 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 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 :: 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 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}

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 A29, XBOOLE_0:def 3;

suppose A30: ( a in Y & b in Y ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )

the InternalRel of L is_strongly_connected_in Y by ORDERS_2:def 7;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A30; :: thesis: verum

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 A23, A31, TARSKI:def 1;
then a1 <= b1 by A28, ORDERS_2:3;
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 A23, A32, TARSKI:def 1;
then a1 <= b1 by A28, ORDERS_2:3;
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 A33, TARSKI:def 1;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A34, ORDERS_2:def 5; :: thesis: verum

end;

end;

end;

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; :: 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 A21, A38, WAYBEL_3:def 1;
d in X by A37, A40, WAYBEL_0:def 20;
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 A24, WAYBEL_4:55;
hence ex m being Element of L st
( x <= m & m is_maximal_in X ` ) by A22; :: thesis: verum