thus product J is reflexive :: thesis: verum

proof

let x be Element of (product J); :: according to YELLOW_0:def 1 :: thesis: x <= x
for i being Element of I holds x . i <= x . i ;
hence x <= x by Th28; :: thesis: verum

end;