let x1, x2, y1, y2 be object ; :: thesis: ( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )
assume {x1,x2} c= {y1,y2} ; :: thesis: ( 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; :: thesis: verum