let R, S be RelStr ; :: thesis: ( R is reflexive & S is reflexive implies R [*] S is reflexive )
assume ( R is reflexive & S is reflexive ) ; :: thesis: R [*] S is reflexive
then A1: ( the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of S is_reflexive_in the carrier of S ) by ORDERS_2:def 2;
A2: ( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) ) by Th2;
the InternalRel of (R [*] S) is_reflexive_in the carrier of (R [*] S)
proof
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in the carrier of (R [*] S) or [x,x] in the InternalRel of (R [*] S) )
assume x in the carrier of (R [*] S) ; :: thesis: [x,x] in the InternalRel of (R [*] S)
then x in the carrier of R \/ the carrier of S by Def2;
then ( x in the carrier of R or x in the carrier of S ) by XBOOLE_0:def 3;
then ( [x,x] in the InternalRel of R or [x,x] in the InternalRel of S ) by A1;
hence [x,x] in the InternalRel of (R [*] S) by A2; :: thesis: verum
end;
hence R [*] S is reflexive by ORDERS_2:def 2; :: thesis: verum