let L be non empty Poset; for c being Function of L,L st c is closure holds
( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )
let c be Function of L,L; ( c is closure implies ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) ) )
A1:
corestr c = c
by Th30;
assume A2:
c is closure
; ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )
then A3:
c is idempotent
by Def13;
[(inclusion c),(corestr c)] is Galois
by A2, Th36;
then A4:
corestr c is lower_adjoint
;
hence
corestr c is sups-preserving
; for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) )
let X be Subset of L; ( X c= the carrier of (Image c) & ex_sup_of X,L implies ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) )
assume that
A5:
X c= the carrier of (Image c)
and
A6:
ex_sup_of X,L
; ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) )
X c= rng c
by A5, YELLOW_0:def 15;
then A7:
c .: X = X
by A3, YELLOW_2:20;
corestr c preserves_sup_of X
by A4, WAYBEL_0:def 33;
hence
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) )
by A6, A1, A7; verum