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 )

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

( p [= q implies the carrier of A1 c= the carrier of A2 )
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;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

proof

hence
( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) )
by A1, A2, A3; :: thesis: verum
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;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