let F be Field; 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; 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; ( 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
; segment (W1,W2) = segment (W3,W4)
thus
segment (W1,W2) c= segment (W3,W4)
XBOOLE_0:def 10 segment (W3,W4) c= segment (W1,W2)proof
let a be
object ;
TARSKI:def 3 ( not a in segment (W1,W2) or a in segment (W3,W4) )
assume A5:
a in segment (
W1,
W2)
;
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;
verum
end;
let a be object ; TARSKI:def 3 ( not a in segment (W3,W4) or a in segment (W1,W2) )
assume A7:
a in segment (W3,W4)
; 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; verum