defpred S1[ Element of Subspaces V, Element of Subspaces V, Element of Subspaces V] means for W1, W2 being Subspace of V st $1 = W1 & $2 = W2 holds
$3 = W1 /\ W2;
A1:
for A1, A2 being Element of Subspaces V ex B being Element of Subspaces V st S1[A1,A2,B]
ex o being BinOp of (Subspaces V) st
for a, b being Element of Subspaces V holds S1[a,b,o . (a,b)]
from BINOP_1:sch 3(A1);
hence
ex b1 being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
; verum