let X be set ; :: thesis: for p being relation st X c= p holds
X is relation
let p be relation; :: thesis: ( X c= p implies X is relation )
assume A1: for x being set st x in X holds
x in p ; :: according to TARSKI:def 3 :: thesis: X is relation
X is FinSequence-membered

proof

let x be set ; :: according to FINSEQ_1:def 19 :: thesis: ( not x in X or x is set )
assume x in X ; :: thesis: x is set
then x in p by A1;
hence x is set ; :: thesis: verum

end;

then reconsider X = X as FinSequence-membered set ;
X is with_common_domain

proof

let a be FinSequence; :: according to MARGREL1:def 1 :: thesis: for b being FinSequence st a in X & b in X holds
len a = len b
let b be FinSequence; :: thesis: ( a in X & b in X implies len a = len b )
assume that
A2: a in X and
A3: b in X ; :: thesis: len a = len b
A4: b in p by A1, A3;
a in p by A1, A2;
hence len a = len b by A4, Def1; :: thesis: verum

end;

hence X is relation ; :: thesis: verum