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:75;
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 e' = @ ((Omega). V) as Element of Submodules V ;
A1: e' = (Omega). V by LMOD_6:def 3;

now

let a' be Element of Submodules V; :: thesis: ( (SubMeet V) . e',a' = a' & (SubMeet V) . a',e' = a' )
reconsider b = a' as Element of Submodules V ;
reconsider a = b as strict Subspace of V ;
thus (SubMeet V) . e',a' = ((Omega). V) /\ a by A1, VECTSP_5:def 8
.= a' by VECTSP_5:27 ; :: thesis: (SubMeet V) . a',e' = a'
thus (SubMeet V) . a',e' = a /\ ((Omega). V) by A1, VECTSP_5:def 8
.= a' by VECTSP_5:27 ; :: thesis: verum

end;

then A2: e' is_a_unity_wrt SubMeet V by BINOP_1:11;
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