let F be Field; :: thesis: for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
let VS be strict VectSp of F; :: thesis: for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
let p, q be Element of (lattice VS); :: thesis: for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
let H1, H2 be strict Subspace of VS; :: thesis: ( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) )
consider A1 being strict Subspace of VS such that
A1: A1 = p by VECTSP_5:def 3;
consider A2 being strict Subspace of VS such that
A2: A2 = q by VECTSP_5:def 3;
A3: ( the carrier of A1 c= the carrier of A2 implies p [= q )

proof

assume the carrier of A1 c= the carrier of A2 ; :: thesis: p [= q
then the carrier of A1 /\ the carrier of A2 = the carrier of A1 by XBOOLE_1:28;
then A4: A1 /\ A2 = A1 by VECTSP_5:def 2;
A1 /\ A2 = the L_meet of (lattice VS) . (p,q) by A1, A2, VECTSP_5:def 8
.= p "/\" q by LATTICES:def 2 ;
hence p [= q by A1, A4, LATTICES:4; :: thesis: verum

end;

( p [= q implies the carrier of A1 c= the carrier of A2 )

proof

assume p [= q ; :: thesis: the carrier of A1 c= the carrier of A2
then A5: p "/\" q = p by LATTICES:4;
p "/\" q = (SubMeet VS) . (p,q) by LATTICES:def 2
.= A1 /\ A2 by A1, A2, VECTSP_5:def 8 ;
then the carrier of A1 /\ the carrier of A2 = the carrier of A1 by A1, A5, VECTSP_5:def 2;
hence the carrier of A1 c= the carrier of A2 by XBOOLE_1:17; :: thesis: verum

end;

hence ( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) ) by A1, A2, A3; :: thesis: verum