let L be up-complete Semilattice; :: thesis: ( SupMap L is meet-preserving implies for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )
assume A1: SupMap L is meet-preserving ; :: thesis: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
set f = SupMap L;
let I1, I2 be Ideal of L; :: thesis: (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
reconsider x = I1, y = I2 as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A2: SupMap L preserves_inf_of {x,y} by A1;
reconsider fx = (SupMap L) . x as Element of L ;
thus (sup I1) "/\" (sup I2) = fx "/\" (sup I2) by YELLOW_2:def 3
.= ((SupMap L) . x) "/\" ((SupMap L) . y) by YELLOW_2:def 3
.= (SupMap L) . (x "/\" y) by A2, YELLOW_3:8
.= (SupMap L) . (I1 "/\" I2) by YELLOW_4:58
.= sup (I1 "/\" I2) by YELLOW_2:def 3 ; :: thesis: verum