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
set y = the Element of Y;
let x be Element of X; :: thesis: x <= x
[x, the Element of Y] <= [x, the Element of 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
set x = the Element of X;
let y be Element of Y; :: thesis: y <= y
[ the Element of X,y] <= [ the Element of 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