let x, y, X be set ; :: thesis: for C being Element of CSp X st {x,y} in C holds
( x in union C & y in union C )
let C be Element of CSp X; :: thesis: ( {x,y} in C implies ( x in union C & y in union C ) )
A1: ( {x} c= {x,y} & {y} c= {x,y} ) by ZFMISC_1:7;
A2: ( x in {x} & y in {y} ) by TARSKI:def 1;
assume {x,y} in C ; :: thesis: ( x in union C & y in union C )
hence ( x in union C & y in union C ) by A1, A2, TARSKI:def 4; :: thesis: verum