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 ` ) )
assume A1: x in X ` ; :: thesis: 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:35;
( x1 c= X ` & x in x1 ) by A1, ZFMISC_1:37;
then A2: x1 in { C where C is Chain of L : ( C c= X ` & x in C ) } ;
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
A3: ( Z <> {} & 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

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:94;
the InternalRel of L is_strongly_connected_in UZ

proof

let a, b be set ; :: 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 A5: ( a in UZ & b in UZ ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then consider az being set such that
A6: ( a in az & az in Z ) by TARSKI:def 4;
consider bz being set such that
A7: ( b in bz & bz in Z ) by A5, TARSKI:def 4;
az,bz are_c=-comparable by A4, A6, A7, ORDINAL1:def 9;
then A8: ( az c= bz or bz c= az ) by XBOOLE_0:def 9;
az in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3, A6;
then ex C being Chain of L st
( az = C & C c= X ` & x in C ) ;
then reconsider az = az as Chain of L ;
bz in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3, A7;
then ex C being Chain of L st
( bz = C & C c= X ` & x in C ) ;
then reconsider bz = bz as Chain of L ;
( the InternalRel of L is_strongly_connected_in az & the InternalRel of L is_strongly_connected_in bz ) by ORDERS_2:def 11;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A6, A7, A8, RELAT_2:def 7; :: thesis: verum

end;

then reconsider UZ = UZ as Chain of L by ORDERS_2:def 11;

now

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;

then A9: UZ c= X ` by ZFMISC_1:94;
consider Y being Element of Z;
Y in Z by A3;
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 ) ;
then x in UZ by A3, TARSKI:def 4;
hence union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } by A9; :: thesis: verum

end;

then consider Y1 being set such that
A10: ( Y1 in { C where C is Chain of L : ( C c= X ` & x in C ) } & ( 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 A2, ORDERS_1:177;
consider Y being Chain of L such that
A11: ( Y = Y1 & Y c= X ` & x in Y ) by A10;
set m = sup Y;
A12: sup Y is_>=_than Y by YELLOW_0:32;

now

assume sup Y in X ; :: thesis: contradiction
then consider y being Element of L such that
A13: ( y in X & y << sup Y ) by Def1;
consider d being Element of L such that
A14: ( d in Y & y <= d ) by A11, A13, WAYBEL_3:def 1;
d in X by A13, A14, WAYBEL_0:def 20;
hence contradiction by A11, A14, XBOOLE_0:def 5; :: thesis: verum

end;

then A15: sup Y in X ` by XBOOLE_0:def 5;
sup Y is_>=_than Y by YELLOW_0:32;
then A16: x <= sup Y by A11, LATTICE3:def 9;

now

given y being Element of L such that A17: ( y in X ` & y > sup Y ) ; :: thesis: contradiction
A18: ( sup Y <= y & sup Y <> y ) by A17, ORDERS_2:def 10;
set Y2 = Y \/ {y};
the InternalRel of L is_strongly_connected_in Y \/ {y}

proof

let a, b be set ; :: 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 A19: ( 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 A19, XBOOLE_0:def 3;

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

end;

suppose A21: ( a in Y & b in {y} ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )

then reconsider b1 = b as Element of L ;
reconsider a1 = a as Element of L by A21;
A22: b1 = y by A21, TARSKI:def 1;
a1 <= sup Y by A12, A21, LATTICE3:def 9;
then a1 <= b1 by A18, A22, ORDERS_2:26;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose A23: ( a in {y} & b in Y ) ; :: thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )

then reconsider b1 = a as Element of L ;
reconsider a1 = b as Element of L by A23;
A24: b1 = y by A23, TARSKI:def 1;
a1 <= sup Y by A12, A23, LATTICE3:def 9;
then a1 <= b1 by A18, A24, ORDERS_2:26;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose A25: ( 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 ;
( a = y & b = y & a1 <= a1 ) by A25, TARSKI:def 1;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

end;

end;

then reconsider Y2 = Y \/ {y} as Chain of L by ORDERS_2:def 11;
{y} c= X ` by A17, ZFMISC_1:37;
then ( Y2 c= X ` & x in Y2 ) by A11, XBOOLE_0:def 3, XBOOLE_1:8;
then A26: Y2 in { C where C is Chain of L : ( C c= X ` & x in C ) } ;

A27: now

assume y in Y ; :: thesis: contradiction
then y <= sup Y by A12, LATTICE3:def 9;
hence contradiction by A17, ORDERS_2:30; :: thesis: verum

end;

y in {y} by TARSKI:def 1;
then y in Y2 by XBOOLE_0:def 3;
hence contradiction by A10, A11, A26, A27, XBOOLE_1:7; :: thesis: verum

end;

then sup Y is_maximal_in X ` by A15, WAYBEL_4:56;
hence ex m being Element of L st
( x <= m & m is_maximal_in X ` ) by A16; :: thesis: verum