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