let L be lower-bounded sup-Semilattice; :: thesis: for x being Element of L
for R1, R2 being Relation of L st R1 c= R2 holds
R1 -below x c= R2 -below x
let x be Element of L; :: thesis: for R1, R2 being Relation of L st R1 c= R2 holds
R1 -below x c= R2 -below x
let R1, R2 be Relation of L; :: thesis: ( R1 c= R2 implies R1 -below x c= R2 -below x )
assume A1: R1 c= R2 ; :: thesis: R1 -below x c= R2 -below x
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in R1 -below x or a in R2 -below x )
assume a in R1 -below x ; :: thesis: a in R2 -below x
then consider b being Element of L such that
A2: ( b = a & [b,x] in R1 ) ;
thus a in R2 -below x by A1, A2; :: thesis: verum