let V be RealLinearSpace; :: thesis: for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let W be Subspace of V; :: thesis: ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
A1: the carrier of (((0). V) /\ W) = the carrier of ((0). V) /\ the carrier of W by Def2
.= {(0. V)} /\ the carrier of W by RLSUB_1:def 3 ;
0. V in W by RLSUB_1:25;
then 0. V in the carrier of W by STRUCT_0:def 5;
then {(0. V)} c= the carrier of W by ZFMISC_1:37;
then ( {(0. V)} /\ the carrier of W = {(0. V)} & the carrier of ((0). V) = {(0. V)} ) by RLSUB_1:def 3, XBOOLE_1:28;
hence ((0). V) /\ W = (0). V by A1, RLSUB_1:38; :: thesis: W /\ ((0). V) = (0). V
hence W /\ ((0). V) = (0). V by Th18; :: thesis: verum