let S be Scott meet-continuous TopLattice; :: thesis: for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }

let F be finite Subset of S; :: thesis: Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }

defpred S_{1}[ set ] means ex UU being Subset-Family of S st

( UU = { (uparrow x) where x is Element of S : x in $1 } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in $1 } );

A1: for b, J being set st b in F & J c= F & S_{1}[J] holds

S_{1}[J \/ {b}]
_{1}[ {} ]

S_{1}[F]
from FINSET_1:sch 2(A47, A40, A1);

then (uparrow F) ^0 = union { (wayabove x) where x is Element of S : x in F } by A42, YELLOW_9:4;

hence Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } by Th26; :: thesis: verum

let F be finite Subset of S; :: thesis: Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }

defpred S

( UU = { (uparrow x) where x is Element of S : x in $1 } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in $1 } );

A1: for b, J being set st b in F & J c= F & S

S

proof

A40:
S
let b, J be set ; :: thesis: ( b in F & J c= F & S_{1}[J] implies S_{1}[J \/ {b}] )

assume that

A2: b in F and

J c= F ; :: thesis: ( not S_{1}[J] or S_{1}[J \/ {b}] )

reconsider bb = b as Element of S by A2;

A3: (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }_{1}[J]
; :: thesis: S_{1}[J \/ {b}]

then consider UU being Subset-Family of S such that

A14: UU = { (uparrow x) where x is Element of S : x in J } and

A15: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J } ;

reconsider I = UU \/ {(uparrow bb)} as Subset-Family of S ;

take I ; :: thesis: ( I = { (uparrow x) where x is Element of S : x in J \/ {b} } & (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } )

thus I = { (uparrow x) where x is Element of S : x in J \/ {b} } :: thesis: (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }

X is upper

hence (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A3, A15, A29, Th28; :: thesis: verum

end;assume that

A2: b in F and

J c= F ; :: thesis: ( not S

reconsider bb = b as Element of S by A2;

A3: (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }

proof

assume
S
{ ((uparrow x) ^0) where x is Element of S : x in J } c= { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }

A6: {b} c= J \/ {b} by XBOOLE_1:7;

b in {b} by TARSKI:def 1;

then (uparrow bb) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A6;

then (uparrow bb) ^0 c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:74;

hence (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A5, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } or a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) )

assume a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } ; :: thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)

then consider A being set such that

A7: a in A and

A8: A in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by TARSKI:def 4;

consider y being Element of S such that

A9: A = (uparrow y) ^0 and

A10: y in J \/ {b} by A8;

end;proof

then A5:
union { ((uparrow x) ^0) where x is Element of S : x in J } c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }
by ZFMISC_1:77;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) ^0) where x is Element of S : x in J } or a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } )

assume a in { ((uparrow x) ^0) where x is Element of S : x in J } ; :: thesis: a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }

then A4: ex y being Element of S st

( a = (uparrow y) ^0 & y in J ) ;

J c= J \/ {b} by XBOOLE_1:7;

hence a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A4; :: thesis: verum

end;assume a in { ((uparrow x) ^0) where x is Element of S : x in J } ; :: thesis: a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }

then A4: ex y being Element of S st

( a = (uparrow y) ^0 & y in J ) ;

J c= J \/ {b} by XBOOLE_1:7;

hence a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A4; :: thesis: verum

A6: {b} c= J \/ {b} by XBOOLE_1:7;

b in {b} by TARSKI:def 1;

then (uparrow bb) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A6;

then (uparrow bb) ^0 c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:74;

hence (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A5, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } or a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) )

assume a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } ; :: thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)

then consider A being set such that

A7: a in A and

A8: A in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by TARSKI:def 4;

consider y being Element of S such that

A9: A = (uparrow y) ^0 and

A10: y in J \/ {b} by A8;

per cases
( y in J or y in {b} )
by A10, XBOOLE_0:def 3;

end;

suppose
y in J
; :: thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)

then
(uparrow y) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J }
;

then A11: a in union { ((uparrow x) ^0) where x is Element of S : x in J } by A7, A9, TARSKI:def 4;

union { ((uparrow x) ^0) where x is Element of S : x in J } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7;

hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A11; :: thesis: verum

end;then A11: a in union { ((uparrow x) ^0) where x is Element of S : x in J } by A7, A9, TARSKI:def 4;

union { ((uparrow x) ^0) where x is Element of S : x in J } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7;

hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A11; :: thesis: verum

suppose A12:
y in {b}
; :: thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)

A13:
(uparrow bb) ^0 c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
by XBOOLE_1:7;

y = b by A12, TARSKI:def 1;

hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A13, A7, A9; :: thesis: verum

end;y = b by A12, TARSKI:def 1;

hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A13, A7, A9; :: thesis: verum

then consider UU being Subset-Family of S such that

A14: UU = { (uparrow x) where x is Element of S : x in J } and

A15: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J } ;

reconsider I = UU \/ {(uparrow bb)} as Subset-Family of S ;

take I ; :: thesis: ( I = { (uparrow x) where x is Element of S : x in J \/ {b} } & (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } )

thus I = { (uparrow x) where x is Element of S : x in J \/ {b} } :: thesis: (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }

proof

A29:
(union UU) \/ (uparrow bb) = union I
thus
I c= { (uparrow x) where x is Element of S : x in J \/ {b} }
:: according to XBOOLE_0:def 10 :: thesis: { (uparrow x) where x is Element of S : x in J \/ {b} } c= I

assume a in { (uparrow x) where x is Element of S : x in J \/ {b} } ; :: thesis: a in I

then consider x being Element of S such that

A22: a = uparrow x and

A23: x in J \/ {b} ;

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (uparrow x) where x is Element of S : x in J \/ {b} } or a in I )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in I or a in { (uparrow x) where x is Element of S : x in J \/ {b} } )

assume A16: a in I ; :: thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }

end;assume A16: a in I ; :: thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }

per cases
( a in UU or a in {(uparrow bb)} )
by A16, XBOOLE_0:def 3;

end;

suppose A17:
a in UU
; :: thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }

A18:
J c= J \/ {b}
by XBOOLE_1:7;

ex x being Element of S st

( a = uparrow x & x in J ) by A17, A14;

hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A18; :: thesis: verum

end;ex x being Element of S st

( a = uparrow x & x in J ) by A17, A14;

hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A18; :: thesis: verum

suppose A19:
a in {(uparrow bb)}
; :: thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }

A20:
b in {b}
by TARSKI:def 1;

A21: {b} c= J \/ {b} by XBOOLE_1:7;

a = uparrow bb by A19, TARSKI:def 1;

hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A20, A21; :: thesis: verum

end;A21: {b} c= J \/ {b} by XBOOLE_1:7;

a = uparrow bb by A19, TARSKI:def 1;

hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A20, A21; :: thesis: verum

assume a in { (uparrow x) where x is Element of S : x in J \/ {b} } ; :: thesis: a in I

then consider x being Element of S such that

A22: a = uparrow x and

A23: x in J \/ {b} ;

proof

for X being Subset of S st X in UU holds
thus
(union UU) \/ (uparrow bb) c= union I
:: according to XBOOLE_0:def 10 :: thesis: union I c= (union UU) \/ (uparrow bb)

assume a in union I ; :: thesis: a in (union UU) \/ (uparrow bb)

then consider A being set such that

A35: a in A and

A36: A in I by TARSKI:def 4;

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union I or a in (union UU) \/ (uparrow bb) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (union UU) \/ (uparrow bb) or a in union I )

assume A30: a in (union UU) \/ (uparrow bb) ; :: thesis: a in union I

end;assume A30: a in (union UU) \/ (uparrow bb) ; :: thesis: a in union I

per cases
( a in union UU or a in uparrow bb )
by A30, XBOOLE_0:def 3;

end;

suppose A31:
a in union UU
; :: thesis: a in union I

A32:
UU c= I
by XBOOLE_1:7;

ex A being set st

( a in A & A in UU ) by A31, TARSKI:def 4;

hence a in union I by A32, TARSKI:def 4; :: thesis: verum

end;ex A being set st

( a in A & A in UU ) by A31, TARSKI:def 4;

hence a in union I by A32, TARSKI:def 4; :: thesis: verum

assume a in union I ; :: thesis: a in (union UU) \/ (uparrow bb)

then consider A being set such that

A35: a in A and

A36: A in I by TARSKI:def 4;

per cases
( A in UU or A in {(uparrow bb)} )
by A36, XBOOLE_0:def 3;

end;

X is upper

proof

then
union UU is upper
by WAYBEL_0:28;
let X be Subset of S; :: thesis: ( X in UU implies X is upper )

assume X in UU ; :: thesis: X is upper

then ex x being Element of S st

( X = uparrow x & x in J ) by A14;

hence X is upper ; :: thesis: verum

end;assume X in UU ; :: thesis: X is upper

then ex x being Element of S st

( X = uparrow x & x in J ) by A14;

hence X is upper ; :: thesis: verum

hence (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A3, A15, A29, Th28; :: thesis: verum

proof

A42:
{ ((uparrow x) ^0) where x is Element of S : x in F } = { (wayabove x) where x is Element of S : x in F }
deffunc H_{1}( Element of S) -> Subset of S = (uparrow $1) ^0 ;

reconsider UU = {} as Subset-Family of S by XBOOLE_1:2;

take UU ; :: thesis: ( UU = { (uparrow x) where x is Element of S : x in {} } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } )

reconsider K = union UU as empty Subset of S ;

A41: K ^0 is empty ;

thus UU = { (uparrow x) where x is Element of S : x in {} } :: thesis: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} }_{1}(x) where x is Element of S : x in {} } = {}
from WAYBEL30:sch 1();

hence (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } by A41; :: thesis: verum

end;reconsider UU = {} as Subset-Family of S by XBOOLE_1:2;

take UU ; :: thesis: ( UU = { (uparrow x) where x is Element of S : x in {} } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } )

reconsider K = union UU as empty Subset of S ;

A41: K ^0 is empty ;

thus UU = { (uparrow x) where x is Element of S : x in {} } :: thesis: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} }

proof

{ H
deffunc H_{2}( Element of S) -> Element of bool the carrier of S = uparrow $1;

{ H_{2}(x) where x is Element of S : x in {} } = {}
from WAYBEL30:sch 1();

hence UU = { (uparrow x) where x is Element of S : x in {} } ; :: thesis: verum

end;{ H

hence UU = { (uparrow x) where x is Element of S : x in {} } ; :: thesis: verum

hence (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } by A41; :: thesis: verum

proof

A47:
F is finite
;
thus
{ ((uparrow x) ^0) where x is Element of S : x in F } c= { (wayabove x) where x is Element of S : x in F }
:: according to XBOOLE_0:def 10 :: thesis: { (wayabove x) where x is Element of S : x in F } c= { ((uparrow x) ^0) where x is Element of S : x in F }

assume a in { (wayabove x) where x is Element of S : x in F } ; :: thesis: a in { ((uparrow x) ^0) where x is Element of S : x in F }

then consider x being Element of S such that

A45: a = wayabove x and

A46: x in F ;

(uparrow x) ^0 = wayabove x by Th25;

hence a in { ((uparrow x) ^0) where x is Element of S : x in F } by A45, A46; :: thesis: verum

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (wayabove x) where x is Element of S : x in F } or a in { ((uparrow x) ^0) where x is Element of S : x in F } )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) ^0) where x is Element of S : x in F } or a in { (wayabove x) where x is Element of S : x in F } )

assume a in { ((uparrow x) ^0) where x is Element of S : x in F } ; :: thesis: a in { (wayabove x) where x is Element of S : x in F }

then consider x being Element of S such that

A43: a = (uparrow x) ^0 and

A44: x in F ;

(uparrow x) ^0 = wayabove x by Th25;

hence a in { (wayabove x) where x is Element of S : x in F } by A43, A44; :: thesis: verum

end;assume a in { ((uparrow x) ^0) where x is Element of S : x in F } ; :: thesis: a in { (wayabove x) where x is Element of S : x in F }

then consider x being Element of S such that

A43: a = (uparrow x) ^0 and

A44: x in F ;

(uparrow x) ^0 = wayabove x by Th25;

hence a in { (wayabove x) where x is Element of S : x in F } by A43, A44; :: thesis: verum

assume a in { (wayabove x) where x is Element of S : x in F } ; :: thesis: a in { ((uparrow x) ^0) where x is Element of S : x in F }

then consider x being Element of S such that

A45: a = wayabove x and

A46: x in F ;

(uparrow x) ^0 = wayabove x by Th25;

hence a in { ((uparrow x) ^0) where x is Element of S : x in F } by A45, A46; :: thesis: verum

S

then (uparrow F) ^0 = union { (wayabove x) where x is Element of S : x in F } by A42, YELLOW_9:4;

hence Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } by Th26; :: thesis: verum