let S be meet-continuous Scott 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: F is finite ;
A2: S₁[ {} ]

proof

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

deffunc H₁( Element of S) -> Subset of S = (uparrow $1) ^0 ;
A3: { H₁(x) where x is Element of S : x in {} } = {} from WAYBEL30:sch 1();
reconsider K = union UU as empty Subset of S ;
K ^0 is empty ;
hence (union UU) ^0 = union { ((uparrow x) ^0 ) where x is Element of S : x in {} } by A3; :: thesis: verum

end;

A4: 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 A5: ( b in F & J c= F ) ; :: thesis: ( not S₁[J] or S₁[J \/ {b}] )
assume S₁[J] ; :: thesis: S₁[J \/ {b}]
then consider UU being Subset-Family of S such that
A6: UU = { (uparrow x) where x is Element of S : x in J } and
A7: (union UU) ^0 = union { ((uparrow x) ^0 ) where x is Element of S : x in J } ;
reconsider bb = b as Element of S by A5;
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 set ; :: 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 A8: 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 A8, XBOOLE_0:def 3;

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

then consider x being Element of S such that
A9: ( a = uparrow x & x in J ) by A6;
J c= J \/ {b} by XBOOLE_1:7;
hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A9; :: thesis: verum

end;

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

then A10: a = uparrow bb by TARSKI:def 1;
( b in {b} & {b} c= J \/ {b} ) by TARSKI:def 1, XBOOLE_1:7;
hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A10; :: thesis: verum

end;

end;

end;

let a be set ; :: 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
A11: ( a = uparrow x & x in J \/ {b} ) ;

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

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

then A12: uparrow x in UU by A6;
UU c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
hence a in I by A11, A12; :: thesis: verum

end;

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

then A13: x = b by TARSKI:def 1;
A14: a in {(uparrow x)} by A11, TARSKI:def 1;
{(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
hence a in I by A13, A14; :: 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 consider x being Element of S such that
A15: ( X = uparrow x & x in J ) by A6;
thus X is upper by A15; :: thesis: verum

end;

then A16: union UU is upper by WAYBEL_0:28;
A17: (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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in (union UU) \/ (uparrow bb) or a in union I )
assume A18: a in (union UU) \/ (uparrow bb) ; :: thesis: a in union I

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

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

then consider A being set such that
A19: ( a in A & A in UU ) by TARSKI:def 4;
UU c= I by XBOOLE_1:7;
hence a in union I by A19, TARSKI:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

let a be set ; :: 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
A22: ( a in A & A in I ) by TARSKI:def 4;

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

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

then A c= union UU by ZFMISC_1:92;
then A23: a in union UU by A22;
union UU c= (union UU) \/ (uparrow bb) by XBOOLE_1:7;
hence a in (union UU) \/ (uparrow bb) by A23; :: thesis: verum

end;

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

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

end;

end;

end;

(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 set ; :: 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 consider y being Element of S such that
A25: ( 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 A25; :: thesis: verum

end;

then A26: 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:95;
A27: b in {b} by TARSKI:def 1;
{b} c= J \/ {b} by XBOOLE_1:7;
then (uparrow bb) ^0 in { ((uparrow x) ^0 ) where x is Element of S : x in J \/ {b} } by A27;
then (uparrow bb) ^0 c= union { ((uparrow x) ^0 ) where x is Element of S : x in J \/ {b} } by ZFMISC_1:92;
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 A26, 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 set ; :: 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
A28: ( a in A & 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
A29: ( A = (uparrow y) ^0 & y in J \/ {b} ) by A28;

per cases ( y in J or y in {b} ) by A29, 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 A30: a in union { ((uparrow x) ^0 ) where x is Element of S : x in J } by A28, A29, 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 A30; :: thesis: verum

end;

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

then A31: y = b by TARSKI:def 1;
(uparrow bb) ^0 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 A28, A29, A31; :: thesis: verum

end;

end;

end;

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

end;

S₁[F] from FINSET_1:sch 2(A1, A2, A4);
then consider UU being Subset-Family of S such that
A32: ( UU = { (uparrow x) where x is Element of S : x in F } & (union UU) ^0 = union { ((uparrow x) ^0 ) where x is Element of S : x in F } ) ;
{ ((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 set ; :: 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
A33: ( a = (uparrow x) ^0 & 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 A33; :: thesis: verum

end;

let a be set ; :: 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
A34: ( a = wayabove x & 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 A34; :: thesis: verum

end;

then (uparrow F) ^0 = union { (wayabove x) where x is Element of S : x in F } by A32, YELLOW_9:4;
hence Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } by Th26; :: thesis: verum