let S be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: 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
for C being Subset of st A = C & A is inaccessible_by_directed_joins holds
C is inaccessible_by_directed_joins
let T be non empty reflexive RelStr ; :: thesis: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) implies for A being Subset of
for C being Subset of st A = C & A is inaccessible_by_directed_joins holds
C is inaccessible_by_directed_joins )
assume A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) ; :: thesis: for A being Subset of
for C being Subset of st A = C & A is inaccessible_by_directed_joins holds
C is inaccessible_by_directed_joins
let A be Subset of ; :: thesis: for C being Subset of st A = C & A is inaccessible_by_directed_joins holds
C is inaccessible_by_directed_joins
let C be Subset of ; :: thesis: ( A = C & A is inaccessible_by_directed_joins implies C is inaccessible_by_directed_joins )
assume that
A2: A = C and
A3: for D being non empty directed Subset of st sup D in A holds
D meets A ; :: according to WAYBEL11:def 1 :: thesis: C is inaccessible_by_directed_joins
let D be non empty directed Subset of ; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" D,T in C or not D misses C )
assume A4: sup D in C ; :: thesis: not D misses C
reconsider E = D as non empty directed Subset of 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; :: thesis: verum