let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
let W, W9, W1 be Subspace of M; :: thesis: ( the carrier of W = the carrier of W9 implies ( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 ) )
assume the carrier of W = the carrier of W9 ; :: thesis: ( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
then A1: the carrier of (W1 /\ W) = the carrier of W1 /\ the carrier of W9 by Def2
.= the carrier of (W1 /\ W9) by Def2 ;
hence W1 /\ W = W1 /\ W9 by VECTSP_4:29; :: thesis: W /\ W1 = W9 /\ W1
thus W /\ W1 = W9 /\ W1 by A1, VECTSP_4:29; :: thesis: verum