let F be Field; :: thesis: for V being VectSp of F
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
segment (W1,W2) = segment (W3,W4)
let V be VectSp of F; :: thesis: for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
segment (W1,W2) = segment (W3,W4)
let W1, W2, W3, W4 be Subspace of V; :: thesis: ( W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 implies segment (W1,W2) = segment (W3,W4) )
assume that
A1: W1 is Subspace of W2 and
A2: W3 is Subspace of W4 and
A3: (Omega). W1 = (Omega). W3 and
A4: (Omega). W2 = (Omega). W4 ; :: thesis: segment (W1,W2) = segment (W3,W4)
thus segment (W1,W2) c= segment (W3,W4) :: according to XBOOLE_0:def 10 :: thesis: segment (W3,W4) c= segment (W1,W2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in segment (W1,W2) or a in segment (W3,W4) )
assume A5: a in segment (W1,W2) ; :: thesis: a in segment (W3,W4)
then ex A1 being strict Subspace of V st A1 = a by VECTSP_5:def 3;
then reconsider A = a as strict Subspace of V ;
A is Subspace of W2 by A1, A5, Def1;
then A is Subspace of (Omega). W2 by Th2;
then A6: A is Subspace of W4 by A4, Th3;
W1 is Subspace of A by A1, A5, Def1;
then (Omega). W1 is Subspace of A by Th4;
then W3 is Subspace of A by A3, Th5;
hence a in segment (W3,W4) by A2, A6, Def1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in segment (W3,W4) or a in segment (W1,W2) )
assume A7: a in segment (W3,W4) ; :: thesis: a in segment (W1,W2)
then ex A1 being strict Subspace of V st A1 = a by VECTSP_5:def 3;
then reconsider A = a as strict Subspace of V ;
A is Subspace of W4 by A2, A7, Def1;
then A is Subspace of (Omega). W4 by Th2;
then A8: A is Subspace of W2 by A4, Th3;
W3 is Subspace of A by A2, A7, Def1;
then (Omega). W3 is Subspace of A by Th4;
then W1 is Subspace of A by A3, Th5;
hence a in segment (W1,W2) by A1, A8, Def1; :: thesis: verum