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; :: thesis: verum