let L be lower-bounded sup-Semilattice; :: thesis: for x being Element of L
for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x
let x be Element of L; :: thesis: for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x
let AR be auxiliary(i) Relation of L; :: thesis: AR -below x c= downarrow x
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in AR -below x or a in downarrow x )
assume a in AR -below x ; :: thesis: a in downarrow x
then consider y1 being Element of L such that
A1: y1 = a and
A2: [y1,x] in AR ;
y1 <= x by A2, Def3;
hence a in downarrow x by A1, WAYBEL_0:17; :: thesis: verum