defpred S_{1}[ object ] means ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,$1) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,$1) = 0 ) );

consider C being Subset of (DivisibleMod L) such that

A1: for v being Element of (DivisibleMod L) holds

( v in C iff S_{1}[v] )
from SUBSET_1:sch 3();

take C ; :: thesis: for v being Vector of (DivisibleMod L) holds

( v in C iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) )

thus for v being Vector of (DivisibleMod L) holds

( v in C iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) by A1; :: thesis: verum

( u in I & (ScProductDM L) . (u,$1) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,$1) = 0 ) );

consider C being Subset of (DivisibleMod L) such that

A1: for v being Element of (DivisibleMod L) holds

( v in C iff S

take C ; :: thesis: for v being Vector of (DivisibleMod L) holds

( v in C iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) )

thus for v being Vector of (DivisibleMod L) holds

( v in C iff ex u being Vector of (EMLat L) st

( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) ) by A1; :: thesis: verum