let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(i) Relation of L
for a, b being object st [a,b] in AR holds
[a,b] in IntRel L
let AR be auxiliary(i) Relation of L; :: thesis: for a, b being object st [a,b] in AR holds
[a,b] in IntRel L
let a, b be object ; :: thesis: ( [a,b] in AR implies [a,b] in IntRel L )
assume A1: [a,b] in AR ; :: thesis: [a,b] in IntRel L
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
a9 <= b9 by A1, Def3;
hence [a,b] in IntRel L by ORDERS_2:def 5; :: thesis: verum