set R = ThetaOrder L;
for x being Element of L holds [x,x] in ThetaOrder L

proof

let x be Element of L; :: thesis: [x,x] in ThetaOrder L
x "/\" x = x by IMeet;
hence [x,x] in ThetaOrder L ; :: thesis: verum

end;

hence ThetaOrder L is reflexive by Ble1; :: thesis: verum