defpred S₁[ 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₁[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