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 = (SubMeet VS) . (p,q) by LATTICES:def 2
.= H1 /\ H2 by A1, A2, VECTSP_5:def 8 ;
hence ( p = H1 & q = H2 implies p "/\" q = H1 /\ H2 ) by A1, A2; :: thesis: verum