let T be lower-bounded continuous Scott TopLattice; :: thesis: for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }

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

set B = { (wayabove x) where x is Element of T : verum } ;

set I = { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ;

set P = { (wayabove x) where x is Element of T : wayabove x c= S } ;

A1: { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } = { (wayabove x) where x is Element of T : wayabove x c= S }

hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; :: thesis: verum

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

set B = { (wayabove x) where x is Element of T : verum } ;

set I = { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ;

set P = { (wayabove x) where x is Element of T : wayabove x c= S } ;

A1: { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } = { (wayabove x) where x is Element of T : wayabove x c= S }

proof

{ (wayabove x) where x is Element of T : verum } is Basis of T
by Lm13;
thus
{ G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } c= { (wayabove x) where x is Element of T : wayabove x c= S }
:: according to XBOOLE_0:def 10 :: thesis: { (wayabove x) where x is Element of T : wayabove x c= S } c= { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) }

assume e in { (wayabove x) where x is Element of T : wayabove x c= S } ; :: thesis: e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) }

then consider x being Element of T such that

A5: e = wayabove x and

A6: wayabove x c= S ;

wayabove x in { (wayabove x) where x is Element of T : verum } ;

hence e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } by A5, A6; :: thesis: verum

end;proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (wayabove x) where x is Element of T : wayabove x c= S } or e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } or e in { (wayabove x) where x is Element of T : wayabove x c= S } )

assume e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; :: thesis: e in { (wayabove x) where x is Element of T : wayabove x c= S }

then consider G being Subset of T such that

A2: e = G and

A3: G in { (wayabove x) where x is Element of T : verum } and

A4: G c= S ;

ex x being Element of T st G = wayabove x by A3;

hence e in { (wayabove x) where x is Element of T : wayabove x c= S } by A2, A4; :: thesis: verum

end;assume e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; :: thesis: e in { (wayabove x) where x is Element of T : wayabove x c= S }

then consider G being Subset of T such that

A2: e = G and

A3: G in { (wayabove x) where x is Element of T : verum } and

A4: G c= S ;

ex x being Element of T st G = wayabove x by A3;

hence e in { (wayabove x) where x is Element of T : wayabove x c= S } by A2, A4; :: thesis: verum

assume e in { (wayabove x) where x is Element of T : wayabove x c= S } ; :: thesis: e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) }

then consider x being Element of T such that

A5: e = wayabove x and

A6: wayabove x c= S ;

wayabove x in { (wayabove x) where x is Element of T : verum } ;

hence e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } by A5, A6; :: thesis: verum

hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; :: thesis: verum