defpred S₁[ Element of HP-WFF ] means not (SetVal V) . V is empty ;
A1: for n being Element of NAT holds S₁[ prop n]

let n be Element of NAT ; :: thesis:
(SetVal V) . (prop n) = V . n by Def2;
hence S₁[ prop n] ; :: thesis:

end;

A2: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] )

let r, s be Element of HP-WFF ; :: thesis:
assume that
A3: not (SetVal V) . r is empty and
A4: not (SetVal V) . s is empty ; :: thesis:
(SetVal V) . (r '&' s) = [:((SetVal V) . r),((SetVal V) . s):] by Def2;
hence not (SetVal V) . (r '&' s) is empty by A3, A4; :: thesis:
(SetVal V) . (r => s) = Funcs (((SetVal V) . r),((SetVal V) . s)) by Def2;
hence S₁[r => s] by A4; :: thesis:

end;