:: VECTSP_8 semantic presentation

K150() is Element of bool K146()
K146() is set
bool K146() is non empty set
K130() is set
bool K130() is non empty set
bool K150() is non empty set
K151() is empty V7() non-empty empty-yielding Function-like one-to-one constant functional Element of K150()
the empty V7() non-empty empty-yielding Function-like one-to-one constant functional set is empty V7() non-empty empty-yielding Function-like one-to-one constant functional set
1 is non empty set
2 is non empty set
K98(K151(),1,2) is non empty set
[:K98(K151(),1,2),K98(K151(),1,2):] is non empty V7() set
[:[:K98(K151(),1,2),K98(K151(),1,2):],K98(K151(),1,2):] is non empty V7() set
bool [:[:K98(K151(),1,2),K98(K151(),1,2):],K98(K151(),1,2):] is non empty set
bool [:K98(K151(),1,2),K98(K151(),1,2):] is non empty set
{} is empty V7() non-empty empty-yielding Function-like one-to-one constant functional set
{{},1} is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
f is set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
{ the non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A} is non empty set
x is set
x is (F,A)
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
Subspaces A is non empty set
f is set
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
f is non empty (F,A)
x is Element of f
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty (F,A)
the carrier of A is non empty set
bool the carrier of A is non empty set
f is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
the carrier of f is non empty set
X1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
x is Element of bool the carrier of A
the carrier of X1 is non empty set
z is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
x is Element of bool the carrier of A
the carrier of z is non empty set
z is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
X1 is Element of bool the carrier of A
the carrier of z is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty (F,A)
the carrier of A is non empty set
bool the carrier of A is non empty Element of bool (bool the carrier of A)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
[:(F,A),(bool the carrier of A):] is non empty V7() set
bool [:(F,A),(bool the carrier of A):] is non empty set
f is set
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
X1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A,X1) is Element of bool the carrier of A
z is Element of bool the carrier of A
z is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
the carrier of z is non empty set
A1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of A1 is non empty set
f is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
x is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
X1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
f . x is Element of bool the carrier of A
the carrier of X1 is non empty set
f is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
x is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
X1 is set
f . X1 is set
x . X1 is set
z is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of z is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty (F,A)
bool (F,A) is non empty set
the carrier of A is non empty set
bool the carrier of A is non empty Element of bool (bool the carrier of A)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
(F,A) is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
[:(F,A),(bool the carrier of A):] is non empty V7() set
bool [:(F,A),(bool the carrier of A):] is non empty set
f is non empty Element of bool (F,A)
(F,A) .: f is Element of bool (bool the carrier of A)
bool (bool the carrier of A) is non empty set
x is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A) . x is Element of bool the carrier of A
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
0. A is V50(A) Element of the carrier of A
the carrier of A is non empty set
(F,A) is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
(F,A) is non empty (F,A)
bool the carrier of A is non empty Element of bool (bool the carrier of A)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
[:(F,A),(bool the carrier of A):] is non empty V7() set
bool [:(F,A),(bool the carrier of A):] is non empty set
f is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
(F,A) . f is set
the carrier of f is non empty set
0. f is V50(f) Element of the carrier of f
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty (F,A)
bool (F,A) is non empty set
the carrier of A is non empty set
bool the carrier of A is non empty Element of bool (bool the carrier of A)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
(F,A) is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
[:(F,A),(bool the carrier of A):] is non empty V7() set
bool [:(F,A),(bool the carrier of A):] is non empty set
f is non empty Element of bool (F,A)
(F,A) .: f is Element of bool (bool the carrier of A)
bool (bool the carrier of A) is non empty set
meet ((F,A) .: f) is Element of bool the carrier of A
x is Element of bool (bool the carrier of A)
meet x is Element of bool the carrier of A
0. A is V50(A) Element of the carrier of A
z is set
z is Element of bool the carrier of A
A1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A) . A1 is Element of bool the carrier of A
the carrier of A1 is non empty set
z is Element of bool the carrier of A
z is Element of the carrier of A
A1 is Element of the carrier of A
z + A1 is Element of the carrier of A
B2 is set
X2 is Element of the carrier of A
A2 is Element of the carrier of A
X2 + A2 is Element of the carrier of A
x is Element of bool the carrier of A
x is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A) . x is Element of bool the carrier of A
the carrier of x is non empty set
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
x + x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
v is Element of the carrier of A
the carrier of F is non empty non trivial set
z is Element of the carrier of F
A1 is Element of the carrier of A
z * A1 is Element of the carrier of A
A2 is set
B2 is Element of bool the carrier of A
v is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A) . v is Element of bool the carrier of A
the carrier of v is non empty set
X2 is Element of the carrier of A
z * X2 is Element of the carrier of A
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of x is non empty set
X1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of X1 is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty (F,A)
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
[: the carrier of (F,A), the carrier of (F,A):] is non empty V7() set
the L_meet of (F,A) is non empty V7() V10([: the carrier of (F,A), the carrier of (F,A):]) V11( the carrier of (F,A)) Function-like V17([: the carrier of (F,A), the carrier of (F,A):]) V21([: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A)) Element of bool [:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):]
[:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):] is non empty V7() set
bool [:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):] is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
[: the carrier of (F,A), the carrier of (F,A):] is non empty V7() set
the L_join of (F,A) is non empty V7() V10([: the carrier of (F,A), the carrier of (F,A):]) V11( the carrier of (F,A)) Function-like V17([: the carrier of (F,A), the carrier of (F,A):]) V21([: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A)) Element of bool [:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):]
[:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):] is non empty V7() set
bool [:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):] is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
f is Element of the carrier of (F,A)
x is Element of the carrier of (F,A)
X1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of X1 is non empty set
the carrier of z is non empty set
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of z is non empty set
the carrier of A1 is non empty set
the carrier of z /\ the carrier of A1 is set
z /\ A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the L_meet of (F,A) is non empty V7() V10([: the carrier of (F,A), the carrier of (F,A):]) V11( the carrier of (F,A)) Function-like V17([: the carrier of (F,A), the carrier of (F,A):]) V21([: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A)) Element of bool [:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):]
[: the carrier of (F,A), the carrier of (F,A):] is non empty V7() set
[:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):] is non empty V7() set
bool [:[: the carrier of (F,A), the carrier of (F,A):], the carrier of (F,A):] is non empty set
the L_meet of (F,A) . (f,x) is Element of the carrier of (F,A)
f "/\" x is Element of the carrier of (F,A)
f "/\" x is Element of the carrier of (F,A)
(SubMeet A) . (f,x) is set
z /\ A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of z /\ the carrier of A1 is set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
f is Element of the carrier of (F,A)
x is Element of the carrier of (F,A)
f "\/" x is Element of the carrier of (F,A)
X1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
X1 + z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
(SubJoin A) . (f,x) is set
z + A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
f is Element of the carrier of (F,A)
x is Element of the carrier of (F,A)
f "/\" x is Element of the carrier of (F,A)
X1 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
X1 /\ z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
(SubMeet A) . (f,x) is set
z /\ A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
F is non empty LattStr
the carrier of F is non empty set
bool the carrier of F is non empty set
A is Element of bool the carrier of F
{ b₁ where b₁ is Element of the carrier of F : b₁ is_less_than A } is set
x is Element of the carrier of F
X1 is Element of the carrier of F
z is Element of the carrier of F
z is Element of the carrier of F
A1 is Element of the carrier of F
z is Element of the carrier of F
A is set
{ b₁ where b₁ is Element of the carrier of F : S₁[b₁] } is set
x is Element of the carrier of F
X1 is Element of the carrier of F
z is Element of the carrier of F
z is Element of the carrier of F
X1 is Element of the carrier of F
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
bool the carrier of (F,A) is non empty set
f is Element of bool the carrier of (F,A)
Top (F,A) is Element of the carrier of (F,A)
x is Element of the carrier of (F,A)
x is Element of the carrier of (F,A)
(F,A) is non empty (F,A)
bool (F,A) is non empty set
x is non empty Element of bool (F,A)
(F,A,x) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
X1 is Element of the carrier of (F,A)
the Element of x is Element of x
z is Element of the carrier of (F,A)
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of A is non empty set
bool the carrier of A is non empty Element of bool (bool the carrier of A)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
(F,A) is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
[:(F,A),(bool the carrier of A):] is non empty V7() set
bool [:(F,A),(bool the carrier of A):] is non empty set
X2 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A) . X2 is Element of bool the carrier of A
the carrier of A1 is non empty set
(F,A) .: x is Element of bool (bool the carrier of A)
bool (bool the carrier of A) is non empty set
meet ((F,A) .: x) is Element of bool the carrier of A
the carrier of (F,A,x) is non empty set
z is Element of the carrier of (F,A)
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of A is non empty set
bool the carrier of A is non empty Element of bool (bool the carrier of A)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
(F,A) is non empty V7() V10((F,A)) V11( bool the carrier of A) Function-like V17((F,A)) V21((F,A), bool the carrier of A) Element of bool [:(F,A),(bool the carrier of A):]
[:(F,A),(bool the carrier of A):] is non empty V7() set
bool [:(F,A),(bool the carrier of A):] is non empty set
(F,A) .: x is Element of bool (bool the carrier of A)
bool (bool the carrier of A) is non empty set
the carrier of A1 is non empty set
X2 is set
A2 is Element of bool the carrier of A
B2 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() (F,A,(F,A))
(F,A) . B2 is Element of bool the carrier of A
v is Element of the carrier of (F,A)
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of x is non empty set
(F,A) . the Element of x is Element of bool the carrier of A
meet ((F,A) .: x) is Element of bool the carrier of A
the carrier of (F,A,x) is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is set
f is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of f is non empty set
bool the carrier of f is non empty set
x is Element of bool the carrier of f
Lin x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
X1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of X1 is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of A is non empty set
f is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of f is non empty set
[: the carrier of A, the carrier of f:] is non empty V7() set
bool [: the carrier of A, the carrier of f:] is non empty set
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
(F,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces f is non empty set
SubJoin f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
[:(Subspaces f),(Subspaces f):] is non empty V7() set
[:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty V7() set
bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty set
SubMeet f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
LattStr(# (Subspaces f),(SubJoin f),(SubMeet f) #) is non empty strict LattStr
the carrier of (F,f) is non empty set
[: the carrier of (F,A), the carrier of (F,f):] is non empty V7() set
bool [: the carrier of (F,A), the carrier of (F,f):] is non empty set
bool the carrier of f is non empty set
x is non empty V7() V10( the carrier of A) V11( the carrier of f) Function-like V17( the carrier of A) V21( the carrier of A, the carrier of f) Element of bool [: the carrier of A, the carrier of f:]
X1 is set
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of z is non empty set
x .: the carrier of z is Element of bool the carrier of f
z is Element of bool the carrier of f
Lin z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
X2 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of X2 is non empty set
x .: the carrier of X2 is Element of bool the carrier of f
Lin (x .: the carrier of X2) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
X1 is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,f)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,f)) Element of bool [: the carrier of (F,A), the carrier of (F,f):]
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of z is non empty set
x .: the carrier of z is Element of bool the carrier of f
X1 . z is set
z is Element of bool the carrier of f
Lin z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
(F,A) is non empty (F,A)
X1 is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,f)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,f)) Element of bool [: the carrier of (F,A), the carrier of (F,f):]
z is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,f)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,f)) Element of bool [: the carrier of (F,A), the carrier of (F,f):]
z is set
X1 . z is set
z . z is set
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of A1 is non empty set
x .: the carrier of A1 is Element of bool the carrier of f
X2 is Element of bool the carrier of f
Lin X2 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
F is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of F is non empty set
A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of A is non empty set
[: the carrier of F, the carrier of A:] is non empty V7() set
bool [: the carrier of F, the carrier of A:] is non empty set
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A is non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A
x is Element of the carrier of F
X1 is Element of the carrier of F
x "/\" X1 is Element of the carrier of F
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . (x "/\" X1) is Element of the carrier of A
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . x is Element of the carrier of A
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . X1 is Element of the carrier of A
( the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . x) "/\" ( the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . X1) is Element of the carrier of A
F is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of F is non empty set
A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of A is non empty set
[: the carrier of F, the carrier of A:] is non empty V7() set
bool [: the carrier of F, the carrier of A:] is non empty set
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A is non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A
x is Element of the carrier of F
X1 is Element of the carrier of F
x "\/" X1 is Element of the carrier of F
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . (x "\/" X1) is Element of the carrier of A
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . x is Element of the carrier of A
the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . X1 is Element of the carrier of A
( the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . x) "\/" ( the non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Homomorphism of F,A . X1) is Element of the carrier of A
F is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of F is non empty set
A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of A is non empty set
[: the carrier of F, the carrier of A:] is non empty V7() set
bool [: the carrier of F, the carrier of A:] is non empty set
f is non empty V7() V10( the carrier of F) V11( the carrier of A) Function-like V17( the carrier of F) V21( the carrier of F, the carrier of A) Element of bool [: the carrier of F, the carrier of A:]
x is Element of the carrier of F
X1 is Element of the carrier of F
x "\/" X1 is Element of the carrier of F
f . (x "\/" X1) is Element of the carrier of A
f . x is Element of the carrier of A
f . X1 is Element of the carrier of A
(f . x) "\/" (f . X1) is Element of the carrier of A
z is Element of the carrier of F
z is Element of the carrier of F
z "/\" z is Element of the carrier of F
f . (z "/\" z) is Element of the carrier of A
f . z is Element of the carrier of A
f . z is Element of the carrier of A
(f . z) "/\" (f . z) is Element of the carrier of A
x is Element of the carrier of F
X1 is Element of the carrier of F
x "\/" X1 is Element of the carrier of F
f . (x "\/" X1) is Element of the carrier of A
f . x is Element of the carrier of A
f . X1 is Element of the carrier of A
(f . x) "\/" (f . X1) is Element of the carrier of A
z is Element of the carrier of F
z is Element of the carrier of F
z "/\" z is Element of the carrier of F
f . (z "/\" z) is Element of the carrier of A
f . z is Element of the carrier of A
f . z is Element of the carrier of A
(f . z) "/\" (f . z) is Element of the carrier of A
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of A is non empty set
f is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of f is non empty set
[: the carrier of A, the carrier of f:] is non empty V7() set
bool [: the carrier of A, the carrier of f:] is non empty set
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
(F,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces f is non empty set
SubJoin f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
[:(Subspaces f),(Subspaces f):] is non empty V7() set
[:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty V7() set
bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty set
SubMeet f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
LattStr(# (Subspaces f),(SubJoin f),(SubMeet f) #) is non empty strict LattStr
the carrier of (F,f) is non empty set
x is non empty V7() V10( the carrier of A) V11( the carrier of f) Function-like V17( the carrier of A) V21( the carrier of A, the carrier of f) Element of bool [: the carrier of A, the carrier of f:]
(F,A,f,x) is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,f)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,f)) Element of bool [: the carrier of (F,A), the carrier of (F,f):]
[: the carrier of (F,A), the carrier of (F,f):] is non empty V7() set
bool [: the carrier of (F,A), the carrier of (F,f):] is non empty set
X1 is Element of the carrier of (F,A)
z is Element of the carrier of (F,A)
X1 "\/" z is Element of the carrier of (F,A)
(F,A,f,x) . (X1 "\/" z) is Element of the carrier of (F,f)
(F,A,f,x) . X1 is Element of the carrier of (F,f)
(F,A,f,x) . z is Element of the carrier of (F,f)
((F,A,f,x) . X1) "\/" ((F,A,f,x) . z) is Element of the carrier of (F,f)
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is Element of the carrier of (F,f)
the carrier of A1 is non empty set
x .: the carrier of A1 is Element of bool the carrier of f
bool the carrier of f is non empty set
Lin (x .: the carrier of A1) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
0. A is V50(A) Element of the carrier of A
A2 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of A2 is non empty set
x .: the carrier of A2 is Element of bool the carrier of f
v is Element of the carrier of f
x is Element of the carrier of f
v + x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x + x is Element of the carrier of A
x . (x + x) is Element of the carrier of f
the carrier of F is non empty non trivial set
v is Element of the carrier of F
x is Element of the carrier of f
v * x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
v * x is Element of the carrier of A
x . (v * x) is Element of the carrier of f
v is Element of the carrier of f
x is Element of the carrier of f
v + x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x + x is Element of the carrier of A
x . (x + x) is Element of the carrier of f
the carrier of F is non empty non trivial set
v is Element of the carrier of F
x is Element of the carrier of f
v * x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
v * x is Element of the carrier of A
x . (v * x) is Element of the carrier of f
A2 + A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of (A2 + A1) is non empty set
x .: the carrier of (A2 + A1) is Element of bool the carrier of f
Lin (x .: the carrier of (A2 + A1)) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
(F,A,f,x) . (A2 + A1) is set
X2 is Element of the carrier of (F,f)
Lin (x .: the carrier of A2) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
dom x is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
x . (0. A) is Element of the carrier of f
v is Element of the carrier of f
v is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of v is non empty set
x is Element of the carrier of f
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of x is non empty set
x + v is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
x is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of x is non empty set
B2 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of B2 is non empty set
x is set
xa1 is set
xa is set
c is Element of the carrier of A
xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
xa1 is set
xa is set
c is Element of the carrier of A
xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
xa1 is Element of the carrier of f
xa is Element of the carrier of f
xa1 + xa is Element of the carrier of f
xa1 is Element of the carrier of f
xa is Element of the carrier of f
xa1 + xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x + c is Element of the carrier of A
x . (x + c) is Element of the carrier of f
the carrier of F is non empty non trivial set
xa1 is Element of the carrier of F
xa is Element of the carrier of f
xa1 * xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
xa1 * c is Element of the carrier of A
x . (xa1 * c) is Element of the carrier of f
the carrier of (x + v) is non empty set
x is set
xa1 is Element of the carrier of f
xa is Element of the carrier of f
xa1 + xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
c + x is Element of the carrier of A
x . (c + x) is Element of the carrier of f
x is set
xa1 is set
xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
x is Element of the carrier of A
v is Element of the carrier of A
x + v is Element of the carrier of A
x . v is Element of the carrier of f
x . x is Element of the carrier of f
(x . x) + (x . v) is Element of the carrier of f
(Lin (x .: the carrier of A2)) + (Lin (x .: the carrier of A1)) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of A is non empty set
f is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of f is non empty set
[: the carrier of A, the carrier of f:] is non empty V7() set
bool [: the carrier of A, the carrier of f:] is non empty set
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
(F,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces f is non empty set
SubJoin f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
[:(Subspaces f),(Subspaces f):] is non empty V7() set
[:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty V7() set
bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty set
SubMeet f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
LattStr(# (Subspaces f),(SubJoin f),(SubMeet f) #) is non empty strict LattStr
the carrier of (F,f) is non empty set
x is non empty V7() V10( the carrier of A) V11( the carrier of f) Function-like V17( the carrier of A) V21( the carrier of A, the carrier of f) Element of bool [: the carrier of A, the carrier of f:]
(F,A,f,x) is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,f)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,f)) Element of bool [: the carrier of (F,A), the carrier of (F,f):]
[: the carrier of (F,A), the carrier of (F,f):] is non empty V7() set
bool [: the carrier of (F,A), the carrier of (F,f):] is non empty set
X1 is Element of the carrier of (F,A)
z is Element of the carrier of (F,A)
X1 "\/" z is Element of the carrier of (F,A)
(F,A,f,x) . (X1 "\/" z) is Element of the carrier of (F,f)
(F,A,f,x) . X1 is Element of the carrier of (F,f)
(F,A,f,x) . z is Element of the carrier of (F,f)
((F,A,f,x) . X1) "\/" ((F,A,f,x) . z) is Element of the carrier of (F,f)
X1 "/\" z is Element of the carrier of (F,A)
(F,A,f,x) . (X1 "/\" z) is Element of the carrier of (F,f)
((F,A,f,x) . X1) "/\" ((F,A,f,x) . z) is Element of the carrier of (F,f)
A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is Element of the carrier of (F,f)
the carrier of A1 is non empty set
x .: the carrier of A1 is Element of bool the carrier of f
bool the carrier of f is non empty set
Lin (x .: the carrier of A1) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
0. A is V50(A) Element of the carrier of A
A2 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
A2 /\ A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of (A2 /\ A1) is non empty set
x .: the carrier of (A2 /\ A1) is Element of bool the carrier of f
Lin (x .: the carrier of (A2 /\ A1)) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
(F,A,f,x) . (A2 /\ A1) is set
the carrier of A2 is non empty set
X2 is Element of the carrier of (F,f)
x .: the carrier of A2 is Element of bool the carrier of f
Lin (x .: the carrier of A2) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
dom x is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
x is Element of the carrier of f
x is Element of the carrier of f
x + x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
xa1 is Element of the carrier of A
x . xa1 is Element of the carrier of f
xa1 + x is Element of the carrier of A
x . (xa1 + x) is Element of the carrier of f
the carrier of F is non empty non trivial set
x is Element of the carrier of F
x is Element of the carrier of f
x * x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x * x is Element of the carrier of A
x . (x * x) is Element of the carrier of f
x is Element of the carrier of f
x is Element of the carrier of f
x + x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
xa1 is Element of the carrier of A
x . xa1 is Element of the carrier of f
xa1 + x is Element of the carrier of A
x . (xa1 + x) is Element of the carrier of f
the carrier of F is non empty non trivial set
x is Element of the carrier of F
x is Element of the carrier of f
x * x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x * x is Element of the carrier of A
x . (x * x) is Element of the carrier of f
x . (0. A) is Element of the carrier of f
v is Element of the carrier of f
v is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of v is non empty set
x is Element of the carrier of f
x is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of x is non empty set
x /\ v is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
xa1 is Element of the carrier of f
xa is Element of the carrier of f
xa1 + xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x + c is Element of the carrier of A
x . (x + c) is Element of the carrier of f
the carrier of F is non empty non trivial set
xa1 is Element of the carrier of F
xa is Element of the carrier of f
xa1 * xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
xa1 * c is Element of the carrier of A
x . (xa1 * c) is Element of the carrier of f
B2 is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of B2 is non empty set
x is non empty V71() V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of x is non empty set
the carrier of (x /\ v) is non empty set
x is set
xa1 is Element of the carrier of f
xa is Element of the carrier of A
x . xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
x is set
xa1 is set
xa is Element of the carrier of f
c is Element of the carrier of A
x . c is Element of the carrier of f
(Lin (x .: the carrier of A2)) /\ (Lin (x .: the carrier of A1)) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
x is set
xa1 is Element of the carrier of A
x . xa1 is Element of the carrier of f
xa is Element of the carrier of A
x . xa is Element of the carrier of f
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of A is non empty set
f is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
the carrier of f is non empty set
[: the carrier of A, the carrier of f:] is non empty V7() set
bool [: the carrier of A, the carrier of f:] is non empty set
x is non empty V7() V10( the carrier of A) V11( the carrier of f) Function-like V17( the carrier of A) V21( the carrier of A, the carrier of f) Element of bool [: the carrier of A, the carrier of f:]
(F,A,f,x) is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,f)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,f)) Element of bool [: the carrier of (F,A), the carrier of (F,f):]
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
(F,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces f is non empty set
SubJoin f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
[:(Subspaces f),(Subspaces f):] is non empty V7() set
[:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty V7() set
bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):] is non empty set
SubMeet f is non empty V7() V10([:(Subspaces f),(Subspaces f):]) V11( Subspaces f) Function-like V17([:(Subspaces f),(Subspaces f):]) V21([:(Subspaces f),(Subspaces f):], Subspaces f) Element of bool [:[:(Subspaces f),(Subspaces f):],(Subspaces f):]
LattStr(# (Subspaces f),(SubJoin f),(SubMeet f) #) is non empty strict LattStr
the carrier of (F,f) is non empty set
[: the carrier of (F,A), the carrier of (F,f):] is non empty V7() set
bool [: the carrier of (F,A), the carrier of (F,f):] is non empty set
dom (F,A,f,x) is non empty Element of bool the carrier of (F,A)
bool the carrier of (F,A) is non empty set
X1 is set
z is set
(F,A,f,x) . X1 is set
(F,A,f,x) . z is set
z is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of z is non empty set
x .: the carrier of z is Element of bool the carrier of f
bool the carrier of f is non empty set
X2 is Element of the carrier of f
A2 is Element of the carrier of f
X2 + A2 is Element of the carrier of f
B2 is Element of the carrier of A
x . B2 is Element of the carrier of f
v is Element of the carrier of A
x . v is Element of the carrier of f
v + B2 is Element of the carrier of A
x . (v + B2) is Element of the carrier of f
the carrier of F is non empty non trivial set
X2 is Element of the carrier of F
A2 is Element of the carrier of f
X2 * A2 is Element of the carrier of f
B2 is Element of the carrier of A
x . B2 is Element of the carrier of f
X2 * B2 is Element of the carrier of A
x . (X2 * B2) is Element of the carrier of f
A1 is Element of bool the carrier of f
0. A is V50(A) Element of the carrier of A
dom x is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
x . (0. A) is Element of the carrier of f
X2 is Element of the carrier of f
(F,A,f,x) . z is set
Lin A1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
X2 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of X2 is non empty set
x .: the carrier of X2 is Element of bool the carrier of f
B2 is Element of the carrier of f
v is Element of the carrier of f
B2 + v is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
x + x is Element of the carrier of A
x . (x + x) is Element of the carrier of f
the carrier of F is non empty non trivial set
B2 is Element of the carrier of F
v is Element of the carrier of f
B2 * v is Element of the carrier of f
x is Element of the carrier of A
x . x is Element of the carrier of f
B2 * x is Element of the carrier of A
x . (B2 * x) is Element of the carrier of f
A2 is Element of bool the carrier of f
(F,A,f,x) . X2 is set
Lin A2 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
B2 is Element of the carrier of f
B2 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of B2 is non empty set
Lin (x .: the carrier of X2) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
v is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of f
the carrier of v is non empty set
F is non empty non degenerated non trivial V71() V91() V97() V99() well-unital distributive V118() V119() V120() L11()
A is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() VectSpStr over F
(F,A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Subspaces A is non empty set
SubJoin A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
[:(Subspaces A),(Subspaces A):] is non empty V7() set
[:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty V7() set
bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):] is non empty set
SubMeet A is non empty V7() V10([:(Subspaces A),(Subspaces A):]) V11( Subspaces A) Function-like V17([:(Subspaces A),(Subspaces A):]) V21([:(Subspaces A),(Subspaces A):], Subspaces A) Element of bool [:[:(Subspaces A),(Subspaces A):],(Subspaces A):]
LattStr(# (Subspaces A),(SubJoin A),(SubMeet A) #) is non empty strict LattStr
the carrier of (F,A) is non empty set
the carrier of A is non empty set
id the carrier of A is non empty V7() V10( the carrier of A) V11( the carrier of A) Function-like one-to-one V17( the carrier of A) V21( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty V7() set
bool [: the carrier of A, the carrier of A:] is non empty set
(F,A,A,(id the carrier of A)) is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,A)) Function-like V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,A)) Element of bool [: the carrier of (F,A), the carrier of (F,A):]
[: the carrier of (F,A), the carrier of (F,A):] is non empty V7() set
bool [: the carrier of (F,A), the carrier of (F,A):] is non empty set
id the carrier of (F,A) is non empty V7() V10( the carrier of (F,A)) V11( the carrier of (F,A)) Function-like one-to-one V17( the carrier of (F,A)) V21( the carrier of (F,A), the carrier of (F,A)) Element of bool [: the carrier of (F,A), the carrier of (F,A):]
x is set
(F,A,A,(id the carrier of A)) . x is set
X1 is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
the carrier of X1 is non empty set
(id the carrier of A) .: the carrier of X1 is Element of bool the carrier of A
bool the carrier of A is non empty set
z is set
z is Element of the carrier of A
(id the carrier of A) . z is Element of the carrier of A
(F,A,A,(id the carrier of A)) . X1 is set
Lin ((id the carrier of A) .: the carrier of X1) is non empty V71() strict V108(F) V109(F) V110(F) V111(F) V118() V119() V120() Subspace of A
z is set
z is Element of the carrier of A
A1 is Element of the carrier of A
(id the carrier of A) . A1 is Element of the carrier of A
dom (F,A,A,(id the carrier of A)) is non empty Element of bool the carrier of (F,A)
bool the carrier of (F,A) is non empty set