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 () )

let V be LeftMod of K; :: thesis:
set S0 = Submodules V;
set S2 = SubMeet V;
reconsider L = LattStr(# (),(),() #) as Lattice by VECTSP_5:57;
SubMeet V = the L_meet of L ;
hence ( SubMeet V is commutative & SubMeet V is associative ) ; :: thesis:
set e = (Omega). V;
reconsider e9 = @ () as Element of Submodules V ;
A1: e9 = (Omega). V by LMOD_6:def 2;
now :: thesis: for a9 being Element of Submodules V holds
( () . (e9,a9) = a9 & () . (a9,e9) = a9 )
let a9 be Element of Submodules V; :: thesis: ( () . (e9,a9) = a9 & () . (a9,e9) = a9 )
reconsider b = a9 as Element of Submodules V ;
reconsider a = b as strict Subspace of V ;
thus () . (e9,a9) = () /\ a by
.= a9 by VECTSP_5:21 ; :: thesis: () . (a9,e9) = a9
thus () . (a9,e9) = a /\ () by
.= a9 by VECTSP_5:21 ; :: thesis: verum
end;
then A2: e9 is_a_unity_wrt SubMeet V by BINOP_1:3;
hence SubMeet V is having_a_unity by SETWISEO:def 2; :: thesis:
thus (Omega). V = the_unity_wrt () by ; :: thesis: verum