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 set ; :: 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 & [y1,x] in AR ) ;
y1 <= x by A1, Def4;
hence a in downarrow x by A1, WAYBEL_0:17; :: thesis: verum