let E be non empty set ; for H, H9 being ZF-formula
for f being Function of VAR,E holds
( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )
let H, H9 be ZF-formula; for f being Function of VAR,E holds
( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )
let f be Function of VAR,E; ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )
A1:
H '&' H9 is conjunctive
;
then A2:
St ((H '&' H9),E) = (St ((the_left_argument_of (H '&' H9)),E)) /\ (St ((the_right_argument_of (H '&' H9)),E))
by Lm3;
H '&' H9 = (the_left_argument_of (H '&' H9)) '&' (the_right_argument_of (H '&' H9))
by A1, ZF_LANG:40;
then A3:
( H = the_left_argument_of (H '&' H9) & H9 = the_right_argument_of (H '&' H9) )
by ZF_LANG:30;
hence
( f in St (H,E) & f in St (H9,E) implies f in St ((H '&' H9),E) )
by A2, XBOOLE_0:def 4; ( f in St ((H '&' H9),E) implies ( f in St (H,E) & f in St (H9,E) ) )
assume
f in St ((H '&' H9),E)
; ( f in St (H,E) & f in St (H9,E) )
hence
( f in St (H,E) & f in St (H9,E) )
by A2, A3, XBOOLE_0:def 4; verum