let x, y, z be bound_QC-variable; :: thesis: for p, q being Element of QC-WFF
for t, s being bound_QC-variable st All (x,y,z,p) = All (t,s,q) holds
( x = t & y = s & All (z,p) = q )
let p, q be Element of QC-WFF ; :: thesis: for t, s being bound_QC-variable st All (x,y,z,p) = All (t,s,q) holds
( x = t & y = s & All (z,p) = q )
let t, s be bound_QC-variable; :: thesis: ( All (x,y,z,p) = All (t,s,q) implies ( x = t & y = s & All (z,p) = q ) )
assume A1: All (x,y,z,p) = All (t,s,q) ; :: thesis: ( x = t & y = s & All (z,p) = q )
hence x = t by Th6; :: thesis: ( y = s & All (z,p) = q )
All (y,z,p) = All (s,q) by A1, Th6;
hence ( y = s & All (z,p) = q ) by Th6; :: thesis: verum