let L be non empty Poset; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum