let X be Subset of [:R,R:]; :: according to WAYBEL_0:def 33 :: thesis: sup_op R preserves_sup_of X
assume A1: ex_sup_of X,[:R,R:] ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (sup_op R) .: X,R & "\/" ((sup_op R) .: X),R = (sup_op R) . ("\/" X,[:R,R:]) )
thus ex_sup_of (sup_op R) .: X,R by YELLOW_0:17; :: thesis: "\/" ((sup_op R) .: X),R = (sup_op R) . ("\/" X,[:R,R:])
then sup_op R preserves_sup_of X by Th25;
hence "\/" ((sup_op R) .: X),R = (sup_op R) . ("\/" X,[:R,R:]) by A1, WAYBEL_0:def 31; :: thesis: verum