let L be lower-bounded sup-Semilattice; 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; for a, b being object st [a,b] in AR holds
[a,b] in IntRel L
let a, b be object ; ( [a,b] in AR implies [a,b] in IntRel L )
assume A1:
[a,b] in AR
; [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; verum