let L be reflexive transitive RelStr ; :: thesis: for R being auxiliary(ii) Relation of L
for C being Subset of L
for x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)

let R be auxiliary(ii) Relation of L; :: thesis: for C being Subset of L
for x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)

let C be Subset of L; :: thesis: for x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)

let x, y be Element of L; :: thesis: ( x <= y implies SetBelow (R,C,x) c= SetBelow (R,C,y) )
assume A1: x <= y ; :: thesis: SetBelow (R,C,x) c= SetBelow (R,C,y)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in SetBelow (R,C,x) or a in SetBelow (R,C,y) )
assume A2: a in SetBelow (R,C,x) ; :: thesis: a in SetBelow (R,C,y)
then reconsider L = L as non empty reflexive RelStr ;
reconsider a = a as Element of L by A2;
A3: a in C by ;
A4: a <= a ;
[a,x] in R by ;
then [a,y] in R by ;
hence a in SetBelow (R,C,y) by ; :: thesis: verum