let T be complete Lawson TopLattice; :: thesis: for A being Subset of T st A is open holds
A is property(S)
defpred S1[ Subset of T] means $1 is property(S) ;
set S = the Scott TopAugmentation of T;
set R = the correct lower TopAugmentation of T;
A1: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
A3: ex K being prebasis of T st
for A being Subset of T st A in K holds
S1[A]
proof
reconsider K = (sigma T) \/ (omega T) as prebasis of T by Def3;
take K ; :: thesis: for A being Subset of T st A in K holds
S1[A]
let A be Subset of T; :: thesis: ( A in K implies S1[A] )
reconsider AS = A as Subset of the Scott TopAugmentation of T by A2;
reconsider AR = A as Subset of the correct lower TopAugmentation of T by A1;
assume A in K ; :: thesis: S1[A]
then ( ( A in sigma T & sigma T = the topology of the Scott TopAugmentation of T ) or ( A in omega T & omega T = the topology of the correct lower TopAugmentation of T ) ) by Def2, XBOOLE_0:def 3, YELLOW_9:51;
then ( AS is open or AR is open ) ;
then ( AS is property(S) or AR is property(S) ) by Th35, WAYBEL11:15;
hence S1[A] by A2, A1, YELLOW12:19; :: thesis: verum
end;
A4: S1[ [#] T] ;
A5: for A1, A2 being Subset of T st S1[A1] & S1[A2] holds
S1[A1 /\ A2] by Lm3;
A6: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
S1[A] ) holds
S1[ union F] by Lm2;
thus for A being Subset of T st A is open holds
S1[A] from WAYBEL19:sch 1(A3, A6, A5, A4); :: thesis: verum