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 b1 being Element of bool (bool the carrier of IT) holds
( not b1 c= the topology of IT or union b1 in the topology of IT ) ) & ( for b1, b2 being Element of bool the carrier of IT holds
( not b1 in the topology of IT or not b2 in the topology of IT or b1 /\ b2 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 b1, b2 being Element of bool the carrier of IT holds
( not b1 in the topology of IT or not b2 in the topology of IT or b1 /\ b2 in the topology of IT )
proof
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
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;
now :: thesis: for X being Subset of IT st X in a holds
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;
then union a is upper by WAYBEL_0:28;
hence union a in the topology of IT by A1, A3, PRE_TOPC:def 2; :: thesis: verum
end;
thus for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
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
proof
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;
a /\ b is upper by A1, A11, A10, WAYBEL_0:29;
hence a /\ b in the topology of IT by A1, A12, PRE_TOPC:def 2; :: thesis: verum
end;