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) ) ) ) )
assume A1: 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 [(inclusion c),(corestr c)] is Galois by Th39;
then corestr c is lower_adjoint by Def12;
hence A2: 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
A3: X c= the carrier of (Image c) and
A4: ex_sup_of X,L ; :: thesis: ( ex_sup_of X, Image c & "\/" X,(Image c) = c . ("\/" X,L) )
A5: corestr c preserves_sup_of X by A2, WAYBEL_0:def 33;
A6: corestr c = c by Th32;
A7: X c= rng c by A3, YELLOW_0:def 15;
c is projection by A1;
then c is idempotent by Def13;
then c .: X = X by A7, YELLOW_2:22;
hence ( ex_sup_of X, Image c & "\/" X,(Image c) = c . ("\/" X,L) ) by A4, A5, A6, WAYBEL_0:def 31; :: thesis: verum