let X be Subset of [:R,R:]; :: according to WAYBEL_0:def 32 :: thesis: inf_op R preserves_inf_of X
assume A1: ex_inf_of X,[:R,R:] ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (inf_op R) .: X,R & "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) )
thus ex_inf_of (inf_op R) .: X,R by YELLOW_0:17; :: thesis: "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:]))
then inf_op R preserves_inf_of X by Th24;
hence "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) by A1; :: thesis: verum