let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(i) Relation of L
for a, b being set st [a,b] in AR holds
[a,b] in IntRel L
let AR be auxiliary(i) Relation of L; :: thesis: for a, b being set st [a,b] in AR holds
[a,b] in IntRel L
let a, b be set ; :: 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 a' = a, b' = b as Element of L by ZFMISC_1:106;
a' <= b' by A1, Def4;
hence [a,b] in IntRel L by ORDERS_2:def 9; :: thesis: verum