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 ) }

( 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;

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

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

assume
x in X `
; :: thesis: ex m being Element of L st
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 ) }

the InternalRel of L is_strongly_connected_in UZ

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 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

then reconsider UZ = union Z as Subset of L by ZFMISC_1:76;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;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

the InternalRel of L is_strongly_connected_in UZ

proof

then reconsider UZ = UZ as Chain of L by ORDERS_2:def 7;
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;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

A14: now :: thesis: for Y being set st Y in Z holds

Y c= X `

set Y = the Element of Z;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;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

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

( 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 )

( 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}

{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;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

then reconsider Y2 = Y \/ {y} as Chain of L by ORDERS_2:def 7;
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 )

end;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;

end;

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;hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A30; :: thesis: verum

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

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

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

{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

now :: thesis: not sup Y in X

then
sup Y in X `
by XBOOLE_0:def 5;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 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

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