defpred S₁[ set , set ] means ex u, v being Element of V st
( $1 = u & $2 = v & are_Prop u,v );
A1: for x being set st x in Proper_Vectors_of V holds
S₁[x,x]

proof

let x be set ; :: thesis: ( x in Proper_Vectors_of V implies S₁[x,x] )
assume x in Proper_Vectors_of V ; :: thesis: S₁[x,x]
then reconsider u = x as Element of V by Def4;
take u ; :: thesis: ex v being Element of V st
( x = u & x = v & are_Prop u,v )
take u ; :: thesis: ( x = u & x = u & are_Prop u,u )
thus ( x = u & x = u & are_Prop u,u ) ; :: thesis: verum

end;

A2: for x, y being set st S₁[x,y] holds
S₁[y,x] ;
A3: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by Th6;
consider R being Equivalence_Relation of Proper_Vectors_of V such that
A4: for x, y being set holds
( [x,y] in R iff ( x in Proper_Vectors_of V & y in Proper_Vectors_of V & S₁[x,y] ) ) from EQREL_1:sch 1(A1, A2, A3);
take R ; :: thesis: for x, y being set holds
( [x,y] in R iff ( x in Proper_Vectors_of V & y in Proper_Vectors_of V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) )
thus for x, y being set holds
( [x,y] in R iff ( x in Proper_Vectors_of V & y in Proper_Vectors_of V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) by A4; :: thesis: verum