let L be complete LATTICE; :: thesis: for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open )
let c be closure Function of L,L; :: thesis: ( Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open )
A1: ( LowerAdj (inclusion c) = corestr c & corestr c = c ) by Th39, WAYBEL_1:32;
A2: ( inclusion c is infs-preserving Function of (Image c),L & ( Image c is directed-sups-inheriting implies inclusion c is directed-sups-preserving ) & ( inclusion c is directed-sups-preserving implies Image c is directed-sups-inheriting ) ) by Th39, Th40;
hence ( Image c is directed-sups-inheriting implies for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open ) by A1, Th32; :: thesis: ( ( for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open ) implies Image c is directed-sups-inheriting )
assume A3: for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open ; :: thesis: Image c is directed-sups-inheriting
consider X being Scott TopAugmentation of Image c, Y being Scott TopAugmentation of L;
( RelStr(# the carrier of X,the InternalRel of X #) = RelStr(# the carrier of (Image c),the InternalRel of (Image c) #) & RelStr(# the carrier of Y,the InternalRel of Y #) = RelStr(# the carrier of L,the InternalRel of L #) ) by YELLOW_9:def 4;
then reconsider f = c as Function of Y,X by A1;
f is open by A3;
hence Image c is directed-sups-inheriting by A1, A2, Th32; :: thesis: verum