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,W2proof
let a be
set ;
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 Th3;
then A6:
A is
Subspace of
W4
by A4, Th4;
W1 is
Subspace of
A
by A1, A5, Def1;
then
(Omega). W1 is
Subspace of
A
by Th5;
then
W3 is
Subspace of
A
by A3, Th6;
hence
a in segment W3,
W4
by A2, A6, Def1;
verum
end;
let a be set ; 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 Th3;
then A8:
A is Subspace of W2
by A4, Th4;
W3 is Subspace of A
by A2, A7, Def1;
then
(Omega). W3 is Subspace of A
by Th5;
then
W1 is Subspace of A
by A3, Th6;
hence
a in segment W1,W2
by A1, A8, Def1; verum