defpred S₁[ object , object ] means ex u, u1, v, v1 being VECTOR of V st
( $1 = [u,u1] & $2 = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y );
set VV = [: the carrier of V, the carrier of V:];
consider P being Relation of [: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:] such that
A1: for x, z being object holds
( [x,z] in P iff ( x in [: the carrier of V, the carrier of V:] & z in [: the carrier of V, the carrier of V:] & S₁[x,z] ) ) from RELSET_1:sch 1();
take P ; :: thesis: for x, z being object holds
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
let x, z be object ; :: thesis: ( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
thus ( [x,z] in P implies ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) by A1; :: thesis: ( ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) implies [x,z] in P )
assume ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ; :: thesis: [x,z] in P
hence [x,z] in P by A1; :: thesis: verum