defpred S_{1}[ 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_{1}[x,x]
;

A2: for x, y being object st S_{1}[x,y] holds

S_{1}[y,x]
;

A3: for x, y, z being object st S_{1}[x,y] & S_{1}[y,z] holds

S_{1}[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_{1}[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

( $1 = u & $2 = v & are_Prop u,v );

A1: for x being object st x in NonZero V holds

S

A2: for x, y being object st S

S

A3: for x, y, z being object st S

S

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

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