let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(i) Relation of L holds AR c= IntRel L
let AR be auxiliary(i) Relation of L; :: thesis: AR c= IntRel L
let a, b be set ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in AR or [a,b] in IntRel L )
assume [a,b] in AR ; :: thesis: [a,b] in IntRel L
hence [a,b] in IntRel L by Lm2; :: thesis: verum