let S be non empty reflexive antisymmetric up-complete RelStr ; for T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
let T be non empty reflexive RelStr ; ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible )
assume A1:
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #)
; for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
let A be Subset of S; for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
let C be Subset of T; ( A = C & A is inaccessible implies C is inaccessible )
assume that
A2:
A = C
and
A3:
for D being non empty directed Subset of S st sup D in A holds
D meets A
; WAYBEL11:def 1 C is inaccessible
let D be non empty directed Subset of T; WAYBEL11:def 1 ( not sup D in C or not D misses C )
assume A4:
sup D in C
; not D misses C
reconsider E = D as non empty directed Subset of S by A1, WAYBEL_0:3;
ex_sup_of E,S
by WAYBEL_0:75;
then
sup D = sup E
by A1, YELLOW_0:26;
hence
not D misses C
by A2, A3, A4; verum