set f = SupMap L;
A1: 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 35 :: thesis: SupMap L preserves_sup_of {x,y}
assume ex_sup_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_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 A1, FUNCT_1:118;
hence ex_sup_of (SupMap L) .: {x,y},L by YELLOW_0:20; :: 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;
A2: ex_sup_of x1 "\/" y1,L by WAYBEL_0:75;
thus sup ((SupMap L) .: {x,y}) = sup {((SupMap L) . x),((SupMap L) . y)} by A1, FUNCT_1:118
.= ((SupMap L) . x) "\/" ((SupMap L) . y) by YELLOW_0:41
.= ((SupMap L) . x) "\/" (sup y1) by YELLOW_2:def 3
.= (sup x1) "\/" (sup y1) by YELLOW_2:def 3
.= sup (x1 "\/" y1) by Th4
.= sup (downarrow (x1 "\/" y1)) by A2, WAYBEL_0:33
.= (SupMap L) . (downarrow (x1 "\/" y1)) by YELLOW_2:def 3
.= (SupMap L) . (x "\/" y) by YELLOW_4:30
.= (SupMap L) . (sup {x,y}) by YELLOW_0:41 ; :: thesis: verum