let V be RealLinearSpace; :: thesis: for W being Subspace of V holds Up W is Subspace-like
let W be Subspace of V; :: thesis: Up W is Subspace-like
0. V in W by RLSUB_1:25;
hence 0. V in Up W by STRUCT_0:def 5; :: according to RUSUB_4:def 8 :: thesis: for x, y being Element of V
for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W )
thus for x, y being Element of V
for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W ) :: thesis: verum

proof

let x, y be Element of V; :: thesis: for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W )
let a be Real; :: thesis: ( x in Up W & y in Up W implies ( x + y in Up W & a * x in Up W ) )
assume A1: ( x in Up W & y in Up W ) ; :: thesis: ( x + y in Up W & a * x in Up W )
reconsider x = x, y = y as Element of V ;
( x in W & y in W ) by A1, STRUCT_0:def 5;
then ( x + y in W & a * x in W ) by RLSUB_1:28, RLSUB_1:29;
hence ( x + y in Up W & a * x in Up W ) by STRUCT_0:def 5; :: thesis: verum

end;