let D be non empty set ; :: thesis: for X being set
for r being Element of relations_on D st X c= r holds
X is Element of relations_on D
let X be set ; :: thesis: for r being Element of relations_on D st X c= r holds
X is Element of relations_on D
let r be Element of relations_on D; :: thesis: ( X c= r implies X is Element of relations_on D )
assume A1: X c= r ; :: thesis: X is Element of relations_on D
then A2: for a, b being FinSequence of D st a in X & b in X holds
len a = len b by Def7;
r c= D * by Def7;
then X c= D * by A1;
hence X is Element of relations_on D by A2, Def7; :: thesis: verum