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 A2, Th15;

A4: a <= a ;

[a,x] in R by A2, Th15;

then [a,y] in R by A4, A1, WAYBEL_4:def 4;

hence a in SetBelow (R,C,y) by A3, Th15; :: thesis: verum

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 A2, Th15;

A4: a <= a ;

[a,x] in R by A2, Th15;

then [a,y] in R by A4, A1, WAYBEL_4:def 4;

hence a in SetBelow (R,C,y) by A3, Th15; :: thesis: verum