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 set ; :: 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,x] in R by A2, Th18;
A4: a in C by A2, Th18;
a <= a ;
then [a,y] in R by A1, A3, WAYBEL_4:def 5;
hence a in SetBelow R,C,y by A4, Th18; :: thesis: verum