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

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