let X, Y be non empty RelStr ; :: thesis: ( [:X,Y:] is reflexive implies ( X is reflexive & Y is reflexive ) )
assume A1: [:X,Y:] is reflexive ; :: thesis: ( X is reflexive & Y is reflexive )
for x being Element of X holds x <= x

proof

consider y being Element of Y;
let x be Element of X; :: thesis: x <= x
[x,y] <= [x,y] by A1, YELLOW_0:def 1;
hence x <= x by Th11; :: thesis: verum

end;

hence X is reflexive by YELLOW_0:def 1; :: thesis: Y is reflexive
for y being Element of Y holds y <= y

proof

consider x being Element of X;
let y be Element of Y; :: thesis: y <= y
[x,y] <= [x,y] by A1, YELLOW_0:def 1;
hence y <= y by Th11; :: thesis: verum

end;

hence Y is reflexive by YELLOW_0:def 1; :: thesis: verum