:: 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

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

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