let IT be TopAugmentation of L; :: thesis: ( IT is Scott implies IT is correct )

assume A1: IT is Scott ; :: thesis: IT is correct

then [#] IT is open ;

hence the carrier of IT in the topology of IT ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b_{1} being Element of bool (bool the carrier of IT) holds

( not b_{1} c= the topology of IT or union b_{1} in the topology of IT ) ) & ( for b_{1}, b_{2} being Element of bool the carrier of IT holds

( not b_{1} in the topology of IT or not b_{2} in the topology of IT or b_{1} /\ b_{2} in the topology of IT ) ) )

thus for a being Subset-Family of IT st a c= the topology of IT holds

union a in the topology of IT :: thesis: for b_{1}, b_{2} being Element of bool the carrier of IT holds

( not b_{1} in the topology of IT or not b_{2} in the topology of IT or b_{1} /\ b_{2} in the topology of IT )

a /\ b in the topology of IT :: thesis: verum

assume A1: IT is Scott ; :: thesis: IT is correct

then [#] IT is open ;

hence the carrier of IT in the topology of IT ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b

( not b

( not b

thus for a being Subset-Family of IT st a c= the topology of IT holds

union a in the topology of IT :: thesis: for b

( not b

proof

thus
for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
let a be Subset-Family of IT; :: thesis: ( a c= the topology of IT implies union a in the topology of IT )

assume A2: a c= the topology of IT ; :: thesis: union a in the topology of IT

A3: union a is inaccessible

hence union a in the topology of IT by A1, A3, PRE_TOPC:def 2; :: thesis: verum

end;assume A2: a c= the topology of IT ; :: thesis: union a in the topology of IT

A3: union a is inaccessible

proof

let D be non empty directed Subset of IT; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" (D,IT) in union a or not D misses union a )

assume sup D in union a ; :: thesis: not D misses union a

then consider A being set such that

A4: sup D in A and

A5: A in a by TARSKI:def 4;

reconsider A = A as Subset of IT by A5;

A is open by A2, A5;

then D meets A by A1, A4, WAYBEL11:def 1;

then consider x being object such that

A6: x in D and

A7: x in A by XBOOLE_0:3;

x in union a by A5, A7, TARSKI:def 4;

hence not D misses union a by A6, XBOOLE_0:3; :: thesis: verum

end;assume sup D in union a ; :: thesis: not D misses union a

then consider A being set such that

A4: sup D in A and

A5: A in a by TARSKI:def 4;

reconsider A = A as Subset of IT by A5;

A is open by A2, A5;

then D meets A by A1, A4, WAYBEL11:def 1;

then consider x being object such that

A6: x in D and

A7: x in A by XBOOLE_0:3;

x in union a by A5, A7, TARSKI:def 4;

hence not D misses union a by A6, XBOOLE_0:3; :: thesis: verum

now :: thesis: for X being Subset of IT st X in a holds

X is upper

then
union a is upper
by WAYBEL_0:28;X is upper

let X be Subset of IT; :: thesis: ( X in a implies X is upper )

assume X in a ; :: thesis: X is upper

then X is open by A2;

hence X is upper by A1; :: thesis: verum

end;assume X in a ; :: thesis: X is upper

then X is open by A2;

hence X is upper by A1; :: thesis: verum

hence union a in the topology of IT by A1, A3, PRE_TOPC:def 2; :: thesis: verum

a /\ b in the topology of IT :: thesis: verum

proof

let a, b be Subset of IT; :: thesis: ( a in the topology of IT & b in the topology of IT implies a /\ b in the topology of IT )

assume that

A8: a in the topology of IT and

A9: b in the topology of IT ; :: thesis: a /\ b in the topology of IT

reconsider a1 = a, b1 = b as Subset of IT ;

A10: b1 is open by A9;

A11: a1 is open by A8;

A12: a /\ b is inaccessible

hence a /\ b in the topology of IT by A1, A12, PRE_TOPC:def 2; :: thesis: verum

end;assume that

A8: a in the topology of IT and

A9: b in the topology of IT ; :: thesis: a /\ b in the topology of IT

reconsider a1 = a, b1 = b as Subset of IT ;

A10: b1 is open by A9;

A11: a1 is open by A8;

A12: a /\ b is inaccessible

proof

a /\ b is upper
by A1, A11, A10, WAYBEL_0:29;
let D be non empty directed Subset of IT; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" (D,IT) in a /\ b or not D misses a /\ b )

assume A13: sup D in a /\ b ; :: thesis: not D misses a /\ b

then sup D in a1 by XBOOLE_0:def 4;

then D meets a1 by A1, A11, WAYBEL11:def 1;

then consider d1 being object such that

A14: d1 in D and

A15: d1 in a1 by XBOOLE_0:3;

sup D in b1 by A13, XBOOLE_0:def 4;

then D meets b1 by A1, A10, WAYBEL11:def 1;

then consider d2 being object such that

A16: d2 in D and

A17: d2 in b1 by XBOOLE_0:3;

reconsider d1 = d1, d2 = d2 as Element of IT by A14, A16;

consider z being Element of IT such that

A18: z in D and

A19: d1 <= z and

A20: d2 <= z by A14, A16, WAYBEL_0:def 1;

A21: z in b1 by A1, A10, A17, A20, WAYBEL_0:def 20;

z in a1 by A1, A11, A15, A19, WAYBEL_0:def 20;

then z in a /\ b by A21, XBOOLE_0:def 4;

hence not D misses a /\ b by A18, XBOOLE_0:3; :: thesis: verum

end;assume A13: sup D in a /\ b ; :: thesis: not D misses a /\ b

then sup D in a1 by XBOOLE_0:def 4;

then D meets a1 by A1, A11, WAYBEL11:def 1;

then consider d1 being object such that

A14: d1 in D and

A15: d1 in a1 by XBOOLE_0:3;

sup D in b1 by A13, XBOOLE_0:def 4;

then D meets b1 by A1, A10, WAYBEL11:def 1;

then consider d2 being object such that

A16: d2 in D and

A17: d2 in b1 by XBOOLE_0:3;

reconsider d1 = d1, d2 = d2 as Element of IT by A14, A16;

consider z being Element of IT such that

A18: z in D and

A19: d1 <= z and

A20: d2 <= z by A14, A16, WAYBEL_0:def 1;

A21: z in b1 by A1, A10, A17, A20, WAYBEL_0:def 20;

z in a1 by A1, A11, A15, A19, WAYBEL_0:def 20;

then z in a /\ b by A21, XBOOLE_0:def 4;

hence not D misses a /\ b by A18, XBOOLE_0:3; :: thesis: verum

hence a /\ b in the topology of IT by A1, A12, PRE_TOPC:def 2; :: thesis: verum