let R be complete connected LATTICE; :: thesis: for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) )
let T be Scott TopAugmentation of R; :: thesis: for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) )
let S be Subset of T; :: thesis: ( S is open iff ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) )
set DD = { ((downarrow x) ` ) where x is Element of T : verum } ;
thus ( not S is open or S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) :: thesis: ( ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) implies S is open )

proof

assume S is open ; :: thesis: ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } )
then A1: ( S is inaccessible_by_directed_joins & S is upper ) ;
assume A2: ( S <> the carrier of T & not S in { ((downarrow x) ` ) where x is Element of T : verum } ) ; :: thesis: contradiction
then A3: ([#] T) \ S <> {} by PRE_TOPC:23;
A4: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) by YELLOW_9:def 4;
then reconsider K = S ` as Subset of R ;
reconsider D = K as non empty directed Subset of T by A3, A4, WAYBEL_0:3;
A5: D misses S by SUBSET_1:43;
reconsider x = sup D as Element of T ;
S ` = downarrow x

proof

thus S ` c= downarrow x :: according to XBOOLE_0:def 10 :: thesis: downarrow x c= S `

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in S ` or a in downarrow x )
assume A6: a in S ` ; :: thesis: a in downarrow x
then reconsider A = a as Element of T ;
x is_>=_than S ` by YELLOW_0:32;
then A <= x by A6, LATTICE3:def 9;
hence a in downarrow x by WAYBEL_0:17; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow x or a in S ` )
assume A7: a in downarrow x ; :: thesis: a in S `
then reconsider A = a as Element of T ;
( A <= x & not x in S ) by A1, A5, A7, WAYBEL11:def 1, WAYBEL_0:17;
then not A in S by A1, WAYBEL_0:def 20;
hence a in S ` by XBOOLE_0:def 5; :: thesis: verum

end;

then (downarrow x) ` = S ;
hence contradiction by A2; :: thesis: verum

end;

assume A8: ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) ; :: thesis: S is open

per cases ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) by A8;

suppose A9: S = the carrier of T ; :: thesis: S is open

A10: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) by YELLOW_9:def 4;
then S = [#] R by A9;
then A11: S is inaccessible_by_directed_joins by A10, YELLOW_9:47;
S is upper

proof

let x, y be Element of T; :: according to WAYBEL_0:def 20 :: thesis: ( not x in S or not x <= y or y in S )
assume ( x in S & x <= y ) ; :: thesis: y in S
thus y in S by A9; :: thesis: verum

end;

hence S is open by A11; :: thesis: verum

end;

suppose S in { ((downarrow x) ` ) where x is Element of T : verum } ; :: thesis: S is open

then consider x being Element of T such that
A12: S = (downarrow x) ` ;
thus S is open by A12, Th23; :: thesis: verum

end;

end;