set A = IntRel L;
for x being Element of L holds [(Bottom L),x] in IntRel L

proof

let x be Element of L; :: thesis: [(Bottom L),x] in IntRel L
Bottom L <= x by YELLOW_0:44;
hence [(Bottom L),x] in IntRel L by ORDERS_2:def 5; :: thesis: verum

end;

hence IntRel L is auxiliary(iv) by Def7; :: thesis: verum