let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice

set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);

for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st A [= C holds

A "\/" (B "/\" C) = (A "\/" B) "/\" C

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice

set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);

for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st A [= C holds

A "\/" (B "/\" C) = (A "\/" B) "/\" C

proof

hence
LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
by Th57, LATTICES:def 12; :: thesis: verum
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: ( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )

assume A1: A [= C ; :: thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C

consider W1 being strict Subspace of M such that

A2: W1 = A by Def3;

consider W3 being strict Subspace of M such that

A3: W3 = C by Def3;

W1 + W3 = (SubJoin M) . (A,C) by A2, A3, Def7

.= A "\/" C by LATTICES:def 1

.= W3 by A1, A3, LATTICES:def 3 ;

then A4: W1 is Subspace of W3 by Th8;

consider W2 being strict Subspace of M such that

A5: W2 = B by Def3;

reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;

reconsider BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;

thus A "\/" (B "/\" C) = (SubJoin M) . (A,(B "/\" C)) by LATTICES:def 1

.= (SubJoin M) . (A,((SubMeet M) . (B,C))) by LATTICES:def 2

.= (SubJoin M) . (A,BC) by A5, A3, Def8

.= W1 + (W2 /\ W3) by A2, Def7

.= (W1 + W2) /\ W3 by A4, Th30

.= (SubMeet M) . (AB,C) by A3, Def8

.= (SubMeet M) . (((SubJoin M) . (A,B)),C) by A2, A5, Def7

.= (SubMeet M) . ((A "\/" B),C) by LATTICES:def 1

.= (A "\/" B) "/\" C by LATTICES:def 2 ; :: thesis: verum

end;assume A1: A [= C ; :: thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C

consider W1 being strict Subspace of M such that

A2: W1 = A by Def3;

consider W3 being strict Subspace of M such that

A3: W3 = C by Def3;

W1 + W3 = (SubJoin M) . (A,C) by A2, A3, Def7

.= A "\/" C by LATTICES:def 1

.= W3 by A1, A3, LATTICES:def 3 ;

then A4: W1 is Subspace of W3 by Th8;

consider W2 being strict Subspace of M such that

A5: W2 = B by Def3;

reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;

reconsider BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;

thus A "\/" (B "/\" C) = (SubJoin M) . (A,(B "/\" C)) by LATTICES:def 1

.= (SubJoin M) . (A,((SubMeet M) . (B,C))) by LATTICES:def 2

.= (SubJoin M) . (A,BC) by A5, A3, Def8

.= W1 + (W2 /\ W3) by A2, Def7

.= (W1 + W2) /\ W3 by A4, Th30

.= (SubMeet M) . (AB,C) by A3, Def8

.= (SubMeet M) . (((SubJoin M) . (A,B)),C) by A2, A5, Def7

.= (SubMeet M) . ((A "\/" B),C) by LATTICES:def 1

.= (A "\/" B) "/\" C by LATTICES:def 2 ; :: thesis: verum