let x1, x2, y1, y2 be object ; ( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )
assume
{x1,x2} c= {y1,y2}
; ( x1 = y1 or x1 = y2 )
then
( {x1,x2} = {} or {x1,x2} = {y1} or {x1,x2} = {y2} or {x1,x2} = {y1,y2} )
by Lm13;
hence
( x1 = y1 or x1 = y2 )
by Th4, Th6; verum