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₁[ 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₁[J] holds
S₁[J \/ {b}]

proof

let b, J be set ; :: thesis: ( b in F & J c= F & S₁[J] implies S₁[J \/ {b}] )
assume that
A2: b in F and
J c= F ; :: thesis: ( not S₁[J] or S₁[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} }

proof

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

proof

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;

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

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;

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;

end;

end;

assume S₁[J] ; :: thesis: S₁[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} }

proof

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

proof

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

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

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;

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;

end;

end;

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

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

suppose A24: x in J ; :: thesis: a in I

A25: UU c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
uparrow x in UU by A24, A14;
hence a in I by A25, A22; :: thesis: verum

end;

suppose A26: x in {b} ; :: thesis: a in I

A27: {(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
A28: a in {(uparrow x)} by A22, TARSKI:def 1;
x = b by A26, TARSKI:def 1;
hence a in I by A27, A28; :: thesis: verum

end;

end;

end;

A29: (union UU) \/ (uparrow bb) = union I

proof

thus (union UU) \/ (uparrow bb) c= union I :: according to XBOOLE_0:def 10 :: thesis: union I c= (union UU) \/ (uparrow bb)

proof

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

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

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;

suppose A33: a in uparrow bb ; :: thesis: a in union I

A34: uparrow bb in {(uparrow bb)} by TARSKI:def 1;
{(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
hence a in union I by A34, A33, TARSKI:def 4; :: thesis: verum

end;

end;

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union I or a in (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;

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

suppose A in UU ; :: thesis: a in (union UU) \/ (uparrow bb)

then A c= union UU by ZFMISC_1:74;
then A37: a in union UU by A35;
union UU c= (union UU) \/ (uparrow bb) by XBOOLE_1:7;
hence a in (union UU) \/ (uparrow bb) by A37; :: thesis: verum

end;

suppose A38: A in {(uparrow bb)} ; :: thesis: a in (union UU) \/ (uparrow bb)

A39: uparrow bb c= (union UU) \/ (uparrow bb) by XBOOLE_1:7;
A = uparrow bb by A38, TARSKI:def 1;
hence a in (union UU) \/ (uparrow bb) by A39, A35; :: thesis: verum

end;

end;

end;

for X being Subset of S st X in UU holds
X is upper

proof

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;

then union UU is upper by WAYBEL_0:28;
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;

A40: S₁[ {} ]

proof

deffunc H₁( 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 {} }

proof

deffunc H₂( Element of S) -> Element of bool the carrier of S = uparrow $1;
{ H₂(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₁(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;

A42: { ((uparrow x) ^0) where x is Element of S : x in F } = { (wayabove x) where x is Element of S : x in F }

proof

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 }

proof

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;

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

A47: F is finite ;
S₁[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