let N be complete Lawson TopLattice; :: thesis: for T being complete LATTICE

for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

let T be complete LATTICE; :: thesis: for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

let A be correct Lawson TopAugmentation of T; :: thesis: ( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) )

assume A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: thesis: TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

A2: omega T = omega N by A1, WAYBEL19:3;

set S = the correct Scott TopAugmentation of T;

set l = the correct lower TopAugmentation of T;

A3: 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;

A4: RelStr(# the carrier of the correct Scott TopAugmentation of T, the InternalRel of the correct Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;

the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T c= bool the carrier of N

reconsider X = X as Subset-Family of N ;

A5: the topology of the correct lower TopAugmentation of T = omega T by WAYBEL19:def 2;

(sigma N) \/ (omega N) is prebasis of N by WAYBEL19:def 3;

then A6: (sigma T) \/ (omega N) is prebasis of N by A1, YELLOW_9:52;

A7: the topology of the correct Scott TopAugmentation of T = sigma T by YELLOW_9:51;

the carrier of N = the carrier of the correct Scott TopAugmentation of T \/ the carrier of the correct lower TopAugmentation of T by A1, A4, A3;

then N is Refinement of the correct Scott TopAugmentation of T, the correct lower TopAugmentation of T by A2, A6, A5, A7, YELLOW_9:def 6;

then A8: the topology of N = UniCl (FinMeetCl X) by YELLOW_9:56

.= lambda T by A1, A5, A7, WAYBEL19:33

.= the topology of A by WAYBEL19:def 4 ;

RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, YELLOW_9:def 4;

hence TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) by A8; :: thesis: verum

for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

let T be complete LATTICE; :: thesis: for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

let A be correct Lawson TopAugmentation of T; :: thesis: ( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) )

assume A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: thesis: TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

A2: omega T = omega N by A1, WAYBEL19:3;

set S = the correct Scott TopAugmentation of T;

set l = the correct lower TopAugmentation of T;

A3: 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;

A4: RelStr(# the carrier of the correct Scott TopAugmentation of T, the InternalRel of the correct Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;

the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T c= bool the carrier of N

proof

then reconsider X = the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T as Subset-Family of N ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T or a in bool the carrier of N )

assume a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T ; :: thesis: a in bool the carrier of N

then ( a in the topology of the correct Scott TopAugmentation of T or a in the topology of the correct lower TopAugmentation of T ) by XBOOLE_0:def 3;

hence a in bool the carrier of N by A1, A4, A3; :: thesis: verum

end;assume a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T ; :: thesis: a in bool the carrier of N

then ( a in the topology of the correct Scott TopAugmentation of T or a in the topology of the correct lower TopAugmentation of T ) by XBOOLE_0:def 3;

hence a in bool the carrier of N by A1, A4, A3; :: thesis: verum

reconsider X = X as Subset-Family of N ;

A5: the topology of the correct lower TopAugmentation of T = omega T by WAYBEL19:def 2;

(sigma N) \/ (omega N) is prebasis of N by WAYBEL19:def 3;

then A6: (sigma T) \/ (omega N) is prebasis of N by A1, YELLOW_9:52;

A7: the topology of the correct Scott TopAugmentation of T = sigma T by YELLOW_9:51;

the carrier of N = the carrier of the correct Scott TopAugmentation of T \/ the carrier of the correct lower TopAugmentation of T by A1, A4, A3;

then N is Refinement of the correct Scott TopAugmentation of T, the correct lower TopAugmentation of T by A2, A6, A5, A7, YELLOW_9:def 6;

then A8: the topology of N = UniCl (FinMeetCl X) by YELLOW_9:56

.= lambda T by A1, A5, A7, WAYBEL19:33

.= the topology of A by WAYBEL19:def 4 ;

RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, YELLOW_9:def 4;

hence TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) by A8; :: thesis: verum