let K be Ring; :: thesis: for V being LeftMod of K holds

( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

let V be LeftMod of K; :: thesis: ( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

set S0 = Submodules V;

set S2 = SubMeet V;

reconsider L = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) as Lattice by VECTSP_5:57;

SubMeet V = the L_meet of L ;

hence ( SubMeet V is commutative & SubMeet V is associative ) ; :: thesis: ( SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

set e = (Omega). V;

reconsider e9 = @ ((Omega). V) as Element of Submodules V ;

A1: e9 = (Omega). V by LMOD_6:def 2;

hence SubMeet V is having_a_unity by SETWISEO:def 2; :: thesis: (Omega). V = the_unity_wrt (SubMeet V)

thus (Omega). V = the_unity_wrt (SubMeet V) by A1, A2, BINOP_1:def 8; :: thesis: verum

( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

let V be LeftMod of K; :: thesis: ( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

set S0 = Submodules V;

set S2 = SubMeet V;

reconsider L = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) as Lattice by VECTSP_5:57;

SubMeet V = the L_meet of L ;

hence ( SubMeet V is commutative & SubMeet V is associative ) ; :: thesis: ( SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

set e = (Omega). V;

reconsider e9 = @ ((Omega). V) as Element of Submodules V ;

A1: e9 = (Omega). V by LMOD_6:def 2;

now :: thesis: for a9 being Element of Submodules V holds

( (SubMeet V) . (e9,a9) = a9 & (SubMeet V) . (a9,e9) = a9 )

then A2:
e9 is_a_unity_wrt SubMeet V
by BINOP_1:3;( (SubMeet V) . (e9,a9) = a9 & (SubMeet V) . (a9,e9) = a9 )

let a9 be Element of Submodules V; :: thesis: ( (SubMeet V) . (e9,a9) = a9 & (SubMeet V) . (a9,e9) = a9 )

reconsider b = a9 as Element of Submodules V ;

reconsider a = b as strict Subspace of V ;

thus (SubMeet V) . (e9,a9) = ((Omega). V) /\ a by A1, VECTSP_5:def 8

.= a9 by VECTSP_5:21 ; :: thesis: (SubMeet V) . (a9,e9) = a9

thus (SubMeet V) . (a9,e9) = a /\ ((Omega). V) by A1, VECTSP_5:def 8

.= a9 by VECTSP_5:21 ; :: thesis: verum

end;reconsider b = a9 as Element of Submodules V ;

reconsider a = b as strict Subspace of V ;

thus (SubMeet V) . (e9,a9) = ((Omega). V) /\ a by A1, VECTSP_5:def 8

.= a9 by VECTSP_5:21 ; :: thesis: (SubMeet V) . (a9,e9) = a9

thus (SubMeet V) . (a9,e9) = a /\ ((Omega). V) by A1, VECTSP_5:def 8

.= a9 by VECTSP_5:21 ; :: thesis: verum

hence SubMeet V is having_a_unity by SETWISEO:def 2; :: thesis: (Omega). V = the_unity_wrt (SubMeet V)

thus (Omega). V = the_unity_wrt (SubMeet V) by A1, A2, BINOP_1:def 8; :: thesis: verum