let V be RealLinearSpace; for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let W be Subspace of V; ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
0. V in W
by RLSUB_1:17;
then
0. V in the carrier of W
by STRUCT_0:def 5;
then
{(0. V)} c= the carrier of W
by ZFMISC_1:31;
then A1:
{(0. V)} /\ the carrier of W = {(0. V)}
by XBOOLE_1:28;
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
;
hence
((0). V) /\ W = (0). V
by A1, RLSUB_1:def 3; W /\ ((0). V) = (0). V
hence
W /\ ((0). V) = (0). V
by Th14; verum