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 Th35;
A2: corestr c = c by WAYBEL_1:30;
A3: inclusion c is infs-preserving Function of (Image c),L by Th35;
A4: ( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving ) by Th36;
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, Th28; :: 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
set X = the Scott TopAugmentation of Image c;
set Y = the Scott TopAugmentation of L;
A6: RelStr(# the carrier of the Scott TopAugmentation of Image c, the InternalRel of the Scott TopAugmentation of Image c #) = RelStr(# the carrier of (Image c), the InternalRel of (Image c) #) by YELLOW_9:def 4;
RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4;
then reconsider f = c as Function of the Scott TopAugmentation of L, the Scott TopAugmentation of Image c by A2, A6;
f is open by A5;
hence Image c is directed-sups-inheriting by A1, A2, A3, A4, Th28; :: thesis: verum