theorem :: WAYBEL_1:55

for L being 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)) ) ) )