defpred S_{1}[ set ] means for b being Element of B holds P . ($1 /\ b) = (P . $1) * (P . b);

consider X being set such that

A1: for x being set holds

( x in X iff ( x in Sigma & S_{1}[x] ) )
from XFAMILY:sch 1();

for x being object st x in X holds

x in Sigma by A1;

then reconsider X = X as Subset of Sigma by TARSKI:def 3;

take X ; :: thesis: for a being Element of Sigma holds

( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )

let a be Element of Sigma; :: thesis: ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )

thus ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) by A1; :: thesis: verum

consider X being set such that

A1: for x being set holds

( x in X iff ( x in Sigma & S

for x being object st x in X holds

x in Sigma by A1;

then reconsider X = X as Subset of Sigma by TARSKI:def 3;

take X ; :: thesis: for a being Element of Sigma holds

( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )

let a be Element of Sigma; :: thesis: ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )

thus ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) by A1; :: thesis: verum