let F be Field; :: thesis: for VS being strict VectSp of F

for p, q being Element of (lattice VS)

for H1, H2 being Subspace of VS st p = H1 & q = H2 holds

p "\/" q = H1 + H2

let VS be strict VectSp of F; :: thesis: for p, q being Element of (lattice VS)

for H1, H2 being Subspace of VS st p = H1 & q = H2 holds

p "\/" q = H1 + H2

let p, q be Element of (lattice VS); :: thesis: for H1, H2 being Subspace of VS st p = H1 & q = H2 holds

p "\/" q = H1 + H2

let H1, H2 be Subspace of VS; :: thesis: ( p = H1 & q = H2 implies p "\/" q = H1 + H2 )

consider H1 being strict Subspace of VS such that

A1: H1 = p by VECTSP_5:def 3;

consider H2 being strict Subspace of VS such that

A2: H2 = q by VECTSP_5:def 3;

p "\/" q = (SubJoin VS) . (p,q) by LATTICES:def 1

.= H1 + H2 by A1, A2, VECTSP_5:def 7 ;

hence ( p = H1 & q = H2 implies p "\/" q = H1 + H2 ) by A1, A2; :: thesis: verum

for p, q being Element of (lattice VS)

for H1, H2 being Subspace of VS st p = H1 & q = H2 holds

p "\/" q = H1 + H2

let VS be strict VectSp of F; :: thesis: for p, q being Element of (lattice VS)

for H1, H2 being Subspace of VS st p = H1 & q = H2 holds

p "\/" q = H1 + H2

let p, q be Element of (lattice VS); :: thesis: for H1, H2 being Subspace of VS st p = H1 & q = H2 holds

p "\/" q = H1 + H2

let H1, H2 be Subspace of VS; :: thesis: ( p = H1 & q = H2 implies p "\/" q = H1 + H2 )

consider H1 being strict Subspace of VS such that

A1: H1 = p by VECTSP_5:def 3;

consider H2 being strict Subspace of VS such that

A2: H2 = q by VECTSP_5:def 3;

p "\/" q = (SubJoin VS) . (p,q) by LATTICES:def 1

.= H1 + H2 by A1, A2, VECTSP_5:def 7 ;

hence ( p = H1 & q = H2 implies p "\/" q = H1 + H2 ) by A1, A2; :: thesis: verum