let A be non empty set ; ( A is c=-linear implies [:(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 ) } ;
assume A1:
A is c=-linear
; [:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A }
A2:
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
object ;
TARSKI:def 3 ( 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 ) }
;
Z in union { [:a,a:] where a is Element of A : a in A }
then consider z being
set such that A3:
Z in z
and A4:
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:]
and
a in A
and
b in A
by A4;
A6:
a,
b are_c=-comparable
by A1;
end;
{ [: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 ) }
then
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:77;
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 A2;
hence
[:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A }
by Th2; verum