let X be set ; :: thesis: for p being relation st X c= p holds
X is relation-like
let p be relation; :: thesis: ( X c= p implies X is relation-like )
assume A1: for x being set st x in X holds
x in p ; :: according to TARSKI:def 3 :: thesis: X is relation-like
thus for x being set st x in X holds
x is FinSequence :: according to MARGREL1:def 1 :: thesis: for a, b being FinSequence st a in X & b in X holds
len a = len b

proof

let x be set ; :: thesis: ( x in X implies x is FinSequence )
assume x in X ; :: thesis: x is FinSequence
then x in p by A1;
hence x is FinSequence by Def1; :: thesis: verum

end;

thus for a, b being FinSequence st a in X & b in X holds
len a = len b :: thesis: verum

proof

let a, b be FinSequence; :: thesis: ( a in X & b in X implies len a = len b )
assume ( a in X & b in X ) ; :: thesis: len a = len b
then ( a in p & b in p ) by A1;
hence len a = len b by Def1; :: thesis: verum

end;