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 5

.= the carrier of W1 /\ the carrier of W2 by RLSUB_2:def 2 ;

for x being object st x in (Up W1) /\ (Up W2) holds

x in Up (W1 /\ W2)

for x being object st x in Up (W1 /\ W2) holds

x in (Up W1) /\ (Up W2)

hence Up (W1 /\ W2) = (Up W1) /\ (Up W2) by A4, XBOOLE_0:def 10; :: thesis: verum

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 5

.= the carrier of W1 /\ the carrier of W2 by RLSUB_2:def 2 ;

for x being object st x in (Up W1) /\ (Up W2) holds

x in Up (W1 /\ W2)

proof

then A4:
(Up W1) /\ (Up W2) c= Up (W1 /\ W2)
;
let x be object ; :: thesis: ( x in (Up W1) /\ (Up W2) implies x in Up (W1 /\ W2) )

assume A2: x in (Up W1) /\ (Up W2) ; :: thesis: x in Up (W1 /\ W2)

then x in Up W2 by XBOOLE_0:def 4;

then A3: x in the carrier of W2 by RUSUB_4:def 5;

x in Up W1 by A2, XBOOLE_0:def 4;

then x in the carrier of W1 by RUSUB_4:def 5;

hence x in Up (W1 /\ W2) by A1, A3, XBOOLE_0:def 4; :: thesis: verum

end;assume A2: x in (Up W1) /\ (Up W2) ; :: thesis: x in Up (W1 /\ W2)

then x in Up W2 by XBOOLE_0:def 4;

then A3: x in the carrier of W2 by RUSUB_4:def 5;

x in Up W1 by A2, XBOOLE_0:def 4;

then x in the carrier of W1 by RUSUB_4:def 5;

hence x in Up (W1 /\ W2) by A1, A3, XBOOLE_0:def 4; :: thesis: verum

for x being object st x in Up (W1 /\ W2) holds

x in (Up W1) /\ (Up W2)

proof

then
Up (W1 /\ W2) c= (Up W1) /\ (Up W2)
;
let x be object ; :: thesis: ( x in Up (W1 /\ W2) implies x in (Up W1) /\ (Up W2) )

assume A5: x in Up (W1 /\ W2) ; :: thesis: x in (Up W1) /\ (Up W2)

then x in the carrier of W2 by A1, XBOOLE_0:def 4;

then A6: x in Up W2 by RUSUB_4:def 5;

x in the carrier of W1 by A1, A5, XBOOLE_0:def 4;

then x in Up W1 by RUSUB_4:def 5;

hence x in (Up W1) /\ (Up W2) by A6, XBOOLE_0:def 4; :: thesis: verum

end;assume A5: x in Up (W1 /\ W2) ; :: thesis: x in (Up W1) /\ (Up W2)

then x in the carrier of W2 by A1, XBOOLE_0:def 4;

then A6: x in Up W2 by RUSUB_4:def 5;

x in the carrier of W1 by A1, A5, XBOOLE_0:def 4;

then x in Up W1 by RUSUB_4:def 5;

hence x in (Up W1) /\ (Up W2) by A6, XBOOLE_0:def 4; :: thesis: verum

hence Up (W1 /\ W2) = (Up W1) /\ (Up W2) by A4, XBOOLE_0:def 10; :: thesis: verum