let p1, p2 be Element of QC-WFF ; :: thesis: for x1, x2, y1, y2, z1, z2 being bound_QC-variable st Ex x1,y1,z1,p1 = Ex x2,y2,z2,p2 holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
let x1, x2, y1, y2, z1, z2 be bound_QC-variable; :: thesis: ( Ex x1,y1,z1,p1 = Ex x2,y2,z2,p2 implies ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) )
assume A1: Ex x1,y1,z1,p1 = Ex x2,y2,z2,p2 ; :: thesis: ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
thus x1 = x2 by A1, Th19; :: thesis: ( y1 = y2 & z1 = z2 & p1 = p2 )
Ex y1,z1,p1 = Ex y2,z2,p2 by A1, Th19;
hence ( y1 = y2 & z1 = z2 & p1 = p2 ) by Th23; :: thesis: verum