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