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