let W be strict Submodule of V; :: thesis: for W1, W2 being Submodule of V st the carrier of W = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } holds
the carrier of W = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) }
let W1, W2 be Submodule of V; :: thesis: ( the carrier of W = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } implies the carrier of W = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } )
set A = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ;
A8: { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } or x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } )
assume x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }
then ex u, v being VECTOR of V st
( x = v + u & v in W2 & u in W1 ) ;
hence x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: verum

end;

{ (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } or x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } )
assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) }
then ex u, v being VECTOR of V st
( x = v + u & v in W1 & u in W2 ) ;
hence x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ; :: thesis: verum

end;

hence ( the carrier of W = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } implies the carrier of W = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ) by A8; :: thesis: verum