let x1, x2, y1, y2 be Variable; :: thesis: ex z1, z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2
( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;
then consider z1, z2 being Variable such that
A1: ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) ;
take z1 ; :: thesis: ex z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2
take z2 ; :: thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
thus (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A1, Th154; :: thesis: verum