let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)
let W1, W2 be Subspace of V; :: thesis: Up (W1 /\ W2) = (Up W1) /\ (Up W2)
A1: Up (W1 /\ W2) = the carrier of (W1 /\ W2) by RUSUB_4:def 6
.= the carrier of W1 /\ the carrier of W2 by RLSUB_2:def 2 ;
for x being set st x in Up (W1 /\ W2) holds
x in (Up W1) /\ (Up W2)

proof

let x be set ; :: thesis: ( x in Up (W1 /\ W2) implies x in (Up W1) /\ (Up W2) )
assume x in Up (W1 /\ W2) ; :: thesis: x in (Up W1) /\ (Up W2)
then ( x in the carrier of W1 & x in the carrier of W2 ) by A1, XBOOLE_0:def 4;
then ( x in Up W1 & x in Up W2 ) by RUSUB_4:def 6;
hence x in (Up W1) /\ (Up W2) by XBOOLE_0:def 4; :: thesis: verum

end;

then A2: Up (W1 /\ W2) c= (Up W1) /\ (Up W2) by TARSKI:def 3;
for x being set st x in (Up W1) /\ (Up W2) holds
x in Up (W1 /\ W2)

proof

let x be set ; :: thesis: ( x in (Up W1) /\ (Up W2) implies x in Up (W1 /\ W2) )
assume x in (Up W1) /\ (Up W2) ; :: thesis: x in Up (W1 /\ W2)
then ( x in Up W1 & x in Up W2 ) by XBOOLE_0:def 4;
then ( x in the carrier of W1 & x in the carrier of W2 ) by RUSUB_4:def 6;
hence x in Up (W1 /\ W2) by A1, XBOOLE_0:def 4; :: thesis: verum

end;

then (Up W1) /\ (Up W2) c= Up (W1 /\ W2) by TARSKI:def 3;
hence Up (W1 /\ W2) = (Up W1) /\ (Up W2) by A2, XBOOLE_0:def 10; :: thesis: verum