let V be RealUnitarySpace; :: thesis: for W1, W2 being Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let W1, W2 be Subspace of V; :: thesis: for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C1 be Coset of W1; :: thesis: for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C2 be Coset of W2; :: thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 )
set v = the Element of C1 /\ C2;
set C = C1 /\ C2;
assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: C1 /\ C2 is Coset of W1 /\ W2
then reconsider v = the Element of C1 /\ C2 as Element of V by TARSKI:def 3;
v in C1 by A1, XBOOLE_0:def 4;
then A2: C1 = v + W1 by RUSUB_1:72;
v in C2 by A1, XBOOLE_0:def 4;
then A3: C2 = v + W2 by RUSUB_1:72;
reconsider v = v as VECTOR of V ;
A4: v + (W1 /\ W2) c= C1 /\ C2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + (W1 /\ W2) or x in C1 /\ C2 )
assume x in v + (W1 /\ W2) ; :: thesis: x in C1 /\ C2
then consider u being VECTOR of V such that
A5: u in W1 /\ W2 and
A6: x = v + u by Lm16;
u in W2 by A5, Th3;
then x in { (v + u2) where u2 is VECTOR of V : u2 in W2 } by A6;
then A7: x in C2 by A3, RUSUB_1:def 4;
u in W1 by A5, Th3;
then x in { (v + u1) where u1 is VECTOR of V : u1 in W1 } by A6;
then x in C1 by A2, RUSUB_1:def 4;
hence x in C1 /\ C2 by A7, XBOOLE_0:def 4; :: thesis: verum

end;

C1 /\ C2 c= v + (W1 /\ W2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) )
assume A8: x in C1 /\ C2 ; :: thesis: x in v + (W1 /\ W2)
then x in C1 by XBOOLE_0:def 4;
then consider u1 being VECTOR of V such that
A9: u1 in W1 and
A10: x = v + u1 by A2, Lm16;
x in C2 by A8, XBOOLE_0:def 4;
then consider u2 being VECTOR of V such that
A11: u2 in W2 and
A12: x = v + u2 by A3, Lm16;
u1 = u2 by A10, A12, RLVECT_1:8;
then u1 in W1 /\ W2 by A9, A11, Th3;
then x in { (v + u) where u is VECTOR of V : u in W1 /\ W2 } by A10;
hence x in v + (W1 /\ W2) by RUSUB_1:def 4; :: thesis: verum

end;

then C1 /\ C2 = v + (W1 /\ W2) by A4;
hence C1 /\ C2 is Coset of W1 /\ W2 by RUSUB_1:def 5; :: thesis: verum