let L be lower-bounded with_suprema Poset; :: thesis: for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR
let AR be auxiliary(iv) Relation of L; :: thesis: AuxBottom L c= AR
let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in AuxBottom L or [a,b] in AR )
assume A1: [a,b] in AuxBottom L ; :: thesis: [a,b] in AR
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
[a9,b9] in AuxBottom L by A1;
then a9 = Bottom L by Def9;
then [a9,b9] in AR by Def6;
hence [a,b] in AR ; :: thesis: verum