let Z be set ; :: thesis: ( ( for z being set st z in Z holds
ex x, y being set st z = [x,y] ) implies ex X, Y being set st Z c= [:X,Y:] )
assume A1: for z being set st z in Z holds
ex x, y being set st z = [x,y] ; :: thesis: ex X, Y being set st Z c= [:X,Y:]
defpred S₁[ set ] means ex y being set st [$1,y] in Z;
consider X being set such that
A2: for x being set holds
( x in X iff ( x in union (union Z) & S₁[x] ) ) from XBOOLE_0:sch 1();
defpred S₂[ set ] means ex x being set st [x,$1] in Z;
consider Y being set such that
A3: for y being set holds
( y in Y iff ( y in union (union Z) & S₂[y] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: ex Y being set st Z c= [:X,Y:]
take Y ; :: thesis: Z c= [:X,Y:]
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in [:X,Y:] )
assume A4: z in Z ; :: thesis: z in [:X,Y:]
then consider x, y being set such that
A5: z = [x,y] by A1;
x in union (union Z) by A4, A5, ZFMISC_1:134;
then A6: x in X by A2, A4, A5;
y in union (union Z) by A4, A5, ZFMISC_1:134;
then y in Y by A3, A4, A5;
hence z in [:X,Y:] by A5, A6, ZFMISC_1:87; :: thesis: verum