let S, T be non empty reflexive transitive antisymmetric complete Scott TopRelStr ; :: thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open )
assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: thesis: for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open
let F be Subset of S; :: thesis: for G being Subset of T st F = G & F is open holds
G is open
let G be Subset of T; :: thesis: ( F = G & F is open implies G is open )
assume that
A2: F = G and
A3: F is open ; :: thesis: G is open
( F is upper & F is inaccessible ) by A3, WAYBEL11:def 4;
then ( G is upper & G is inaccessible ) by A1, A2, Th47, WAYBEL_0:25;
hence G is open by WAYBEL11:def 4; :: thesis: verum