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 }
proof
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 ) }
proof
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;
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 ) } )
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;
{ (wayabove x) where x is Element of T : verum } is Basis of T by Lm13;
hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; :: thesis: verum