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 } )

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 ; :: thesis: [:(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 }

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; :: thesis: verum

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 ; :: thesis: [:(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

{ [: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 ) }
let Z be object ; :: 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

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;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

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;

per cases
( a c= b or b c= a )
by A6;

end;

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

A8:
[:b,b:] in { [:a,a:] where a is Element of A : a in A }
;

[:a,b:] c= [:b,b:] by A7, ZFMISC_1:95;

hence Z in union { [:a,a:] where a is Element of A : a in A } by A3, A5, A8, TARSKI:def 4; :: thesis: verum

end;[:a,b:] c= [:b,b:] by A7, ZFMISC_1:95;

hence Z in union { [:a,a:] where a is Element of A : a in A } by A3, A5, A8, TARSKI:def 4; :: thesis: verum

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

A10:
[:a,a:] in { [:a,a:] where a is Element of A : a in A }
;

[:a,b:] c= [:a,a:] by A9, ZFMISC_1:95;

hence Z in union { [:a,a:] where a is Element of A : a in A } by A3, A5, A10, TARSKI:def 4; :: thesis: verum

end;[:a,b:] c= [:a,a:] by A9, ZFMISC_1:95;

hence Z in union { [:a,a:] where a is Element of A : a in A } by A3, A5, A10, TARSKI:def 4; :: thesis: verum

proof

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;
let Z be object ; :: 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 ex a being Element of A st

( Z = [:a,a:] & a in A ) ;

hence Z in { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } ; :: thesis: verum

end;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 ex a being Element of A st

( Z = [:a,a:] & a in A ) ;

hence Z in { [:a,b:] where a, b is Element of A : ( a in A & b in A ) } ; :: thesis: verum

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; :: thesis: verum