let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(i) Relation of L
for x being Element of L st AR = the InternalRel of L holds
AR -below x = downarrow x
let AR be auxiliary(i) Relation of L; :: thesis: for x being Element of L st AR = the InternalRel of L holds
AR -below x = downarrow x
let x be Element of L; :: thesis: ( AR = the InternalRel of L implies AR -below x = downarrow x )
assume A1: AR = the InternalRel of L ; :: thesis: AR -below x = downarrow x
thus AR -below x c= downarrow x by Th12; :: according to XBOOLE_0:def 10 :: thesis: downarrow x c= AR -below x
thus downarrow x c= AR -below x :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow x or a in AR -below x )
assume a in downarrow x ; :: thesis: a in AR -below x
then [a,x] in AR by A1, Lm3;
hence a in AR -below x by Th13; :: thesis: verum
end;