let
V
be
RealLinearSpace
;
:: thesis:
for
W
being
strict
Subspace
of
V
holds
W
/\
W
=
W
let
W
be
strict
Subspace
of
V
;
:: thesis:
W
/\
W
=
W
the
carrier
of
W
=
the
carrier
of
W
/\
the
carrier
of
W
;
hence
W
/\
W
=
W
by
Def2
;
:: thesis:
verum