let A be non empty set ; :: thesis: ( A is c=-linear implies [:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A } )
assume A1: A is c=-linear ; :: thesis: [:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A }
set X = { [:a,a:] where a is Element of A : a in A } ;
set Y = { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } ;
{ [:a,a:] where a is Element of A : a in A } c= { [:a,b:] where a, b is Element of A : ( a in A & b in A ) }

proof

let Z be set ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:a,a:] where a is Element of A : a in A } or Z in { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } )
assume Z in { [:a,a:] where a is Element of A : a in A } ; :: thesis: Z in { [:a,b:] where a, b is Element of A : ( a in A & b in A ) }
then consider a being Element of A such that
A2: ( Z = [:a,a:] & a in A ) ;
thus Z in { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } by A2; :: thesis: verum

end;

then A3: union { [:a,a:] where a is Element of A : a in A } c= union { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } by ZFMISC_1:95;
union { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } c= union { [:a,a:] where a is Element of A : a in A }

proof

let Z be set ; :: according to TARSKI:def 3 :: thesis: ( not Z in union { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } or Z in union { [:a,a:] where a is Element of A : a in A } )
assume Z in union { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } ; :: thesis: Z in union { [:a,a:] where a is Element of A : a in A }
then consider z being set such that
A4: ( Z in z & z in { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } ) by TARSKI:def 4;
consider a, b being Element of A such that
A5: ( z = [:a,b:] & a in A & b in A ) by A4;
A6: a,b are_c=-comparable by A1, ORDINAL1:def 9;

per cases ( a c= b or b c= a ) by A6, XBOOLE_0:def 9;

suppose a c= b ; :: thesis: Z in union { [:a,a:] where a is Element of A : a in A }

then [:a,b:] c= [:b,b:] by ZFMISC_1:118;
then ( Z in [:b,b:] & [:b,b:] in { [:a,a:] where a is Element of A : a in A } ) by A4, A5;
hence Z in union { [:a,a:] where a is Element of A : a in A } by TARSKI:def 4; :: thesis: verum

end;

suppose b c= a ; :: thesis: Z in union { [:a,a:] where a is Element of A : a in A }

then [:a,b:] c= [:a,a:] by ZFMISC_1:118;
then ( Z in [:a,a:] & [:a,a:] in { [:a,a:] where a is Element of A : a in A } ) by A4, A5;
hence Z in union { [:a,a:] where a is Element of A : a in A } by TARSKI:def 4; :: thesis: verum

end;

end;

end;

then union { [:a,a:] where a is Element of A : a in A } = union { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } by A3, XBOOLE_0:def 10;
hence [:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A } by Th2; :: thesis: verum