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 object ; :: 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 ex b being Element of L st
( b = a & [b,x] in R1 ) ;
hence a in R2 -below x by A1; :: thesis: verum