let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let W be Subspace of V; :: thesis: for v1, v2 being VECTOR of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let v1, v2 be VECTOR of V; :: thesis: ( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
thus ( ex C being Coset of W st
( v1 in C & v2 in C ) implies v1 - v2 in W ) :: thesis: ( v1 - v2 in W implies ex C being Coset of W st
( v1 in C & v2 in C ) )

proof

given C being Coset of W such that A1: ( v1 in C & v2 in C ) ; :: thesis: v1 - v2 in W
ex v being VECTOR of V st C = v + W by Def5;
hence v1 - v2 in W by A1, Th59; :: thesis: verum

end;

assume v1 - v2 in W ; :: thesis: ex C being Coset of W st
( v1 in C & v2 in C )
then consider v being VECTOR of V such that
A2: ( v1 in v + W & v2 in v + W ) by Th59;
reconsider C = v + W as Coset of W by Def5;
take C ; :: thesis: ( v1 in C & v2 in C )
thus ( v1 in C & v2 in C ) by A2; :: thesis: verum