let R, S be Relation; :: thesis: for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds
R * S is_reflexive_in Y
let Y be set ; :: thesis: ( R is_reflexive_in Y & S is_reflexive_in Y implies R * S is_reflexive_in Y )
assume A1: ( R is_reflexive_in Y & S is_reflexive_in Y ) ; :: thesis: R * S is_reflexive_in Y
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in Y or [x,x] in R * S )
assume x in Y ; :: thesis: [x,x] in R * S
then ( [x,x] in R & [x,x] in S ) by A1;
hence [x,x] in R * S by RELAT_1:def 8; :: thesis: verum