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 by Th39;
A2: corestr c = c by WAYBEL_1:32;
A3: inclusion c is infs-preserving Function of (Image c),L by Th39;
A4: ( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving ) by 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, A2, A3, 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 A5: 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;
A6: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of (Image c), the InternalRel of (Image c) #) by YELLOW_9:def 4;
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 A2, A6;
f is open by A5;
hence Image c is directed-sups-inheriting by A1, A2, A3, A4, Th32; :: thesis: verum