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 A1: S is open ; :: thesis: ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } )
assume that
A2: S <> the carrier of T and
A3: not S in { ((downarrow x) ` ) where x is Element of T : verum } ; :: thesis: contradiction
A4: ([#] T) \ S <> {} by A2, PRE_TOPC:23;
A5: 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 A4, A5, WAYBEL_0:3;
A6: 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 A7: 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 A7, 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 A8: a in downarrow x ; :: thesis: a in S `
then reconsider A = a as Element of T ;
A9: A <= x by A8, WAYBEL_0:17;
not x in S by A1, A6, WAYBEL11:def 1;
then not A in S by A1, A9, WAYBEL_0:def 20;
hence a in S ` by XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

assume A10: ( 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 A10;

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

A12: 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 A11;
then A13: S is inaccessible_by_directed_joins by A12, 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 that
x in S and
x <= y ; :: thesis: y in S
thus y in S by A11; :: thesis: verum

end;

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

end;

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

then ex x being Element of T st S = (downarrow x) ` ;
hence S is open by Th23; :: thesis: verum

end;

end;