let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def 35 :: thesis: SupMap L preserves_sup_of {x,y}
set f = SupMap L;
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)))) )
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41;
A1: ex_sup_of x1 "\/" y1,L by WAYBEL_0:75;
A2: dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def 1;
then (SupMap L) .: {x,y} = {((SupMap L) . x),((SupMap L) . y)} by FUNCT_1:60;
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))))
thus sup ((SupMap L) .: {x,y}) = sup {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:60
.= ((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 A1, 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