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:
let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def 34 :: thesis:
set f = SupMap L;
assume ex_inf_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of () .: {x,y},L & "/\" ((() .: {x,y}),L) = () . ("/\" ({x,y},(InclPoset (Ids L)))) )
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41;
A2: dom () = the carrier of (InclPoset (Ids L)) by FUNCT_2:def 1;
then (SupMap L) .: {x,y} = {(() . x),(() . y)} by FUNCT_1:60;
hence ex_inf_of () .: {x,y},L by YELLOW_0:21; :: thesis: "/\" ((() .: {x,y}),L) = () . ("/\" ({x,y},(InclPoset (Ids L))))
thus inf (() .: {x,y}) = inf {(() . x),(() . y)} by
.= (() . x) "/\" (() . y) by YELLOW_0:40
.= (() . x) "/\" (sup y1) by YELLOW_2:def 3
.= (sup x1) "/\" (sup y1) by YELLOW_2:def 3
.= sup (x1 "/\" y1) by A1
.= () . (x1 "/\" y1) by YELLOW_2:def 3
.= () . (x "/\" y) by YELLOW_4:58
.= () . (inf {x,y}) by YELLOW_0:40 ; :: thesis: verum