let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(ii) Relation of L
for x, y being Element of L st x <= y holds
AR -below x c= AR -below y
let AR be auxiliary(ii) Relation of L; :: thesis: for x, y being Element of L st x <= y holds
AR -below x c= AR -below y
let x, y be Element of L; :: thesis: ( x <= y implies AR -below x c= AR -below y )
assume A1: x <= y ; :: thesis: AR -below x c= AR -below y
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in AR -below x or a in AR -below y )
assume a in AR -below x ; :: thesis: a in AR -below y
then consider y2 being Element of L such that
A2: y2 = a and
A3: [y2,x] in AR ;
y2 <= y2 ;
then [y2,y] in AR by A1, A3, Def4;
hence a in AR -below y by A2; :: thesis: verum