let L be up-complete Semilattice; :: thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies SupMap L is meet-preserving )
assume A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; :: thesis: SupMap L is meet-preserving
set f = SupMap L;
A2: dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def 1;
let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def 34 :: thesis: SupMap L preserves_inf_of {x,y}
assume ex_inf_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (SupMap L) .: {x,y},L & "/\" ((SupMap L) .: {x,y}),L = (SupMap L) . ("/\" {x,y},(InclPoset (Ids L))) )
(SupMap L) .: {x,y} = {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:118;
hence ex_inf_of (SupMap L) .: {x,y},L by YELLOW_0:21; :: thesis: "/\" ((SupMap L) .: {x,y}),L = (SupMap L) . ("/\" {x,y},(InclPoset (Ids L)))
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:43;
thus inf ((SupMap L) .: {x,y}) = inf {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:118
.= ((SupMap L) . x) "/\" ((SupMap L) . y) by YELLOW_0:40
.= ((SupMap L) . x) "/\" (sup y1) by YELLOW_2:def 3
.= (sup x1) "/\" (sup y1) by YELLOW_2:def 3
.= sup (x1 "/\" y1) by A1
.= (SupMap L) . (x1 "/\" y1) by YELLOW_2:def 3
.= (SupMap L) . (x "/\" y) by YELLOW_4:58
.= (SupMap L) . (inf {x,y}) by YELLOW_0:40 ; :: thesis: verum