:: deftheorem Def8 defines SubMeet RLSUB_2:def 8 :
for V being RealLinearSpace
for b₂ being BinOp of (Subspaces V) holds
( b₂ = SubMeet V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₂ . (A1,A2) = W1 /\ W2 );