let F be Field; 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; 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); for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "\/" q = H1 + H2
let H1, H2 be Subspace of VS; ( 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; verum