let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; :: thesis: for x being set st x in the carrier of R holds
x is Element of (R [*] S)
let x be set ; :: thesis: ( x in the carrier of R implies x is Element of (R [*] S) )
assume x in the carrier of R ; :: thesis: x is Element of (R [*] S)
then x in the carrier of R \/ the carrier of S by XBOOLE_0:def 3;
hence x is Element of (R [*] S) by Def2; :: thesis: verum