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 }
proof
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;
per cases ( a c= b or b c= a ) by A6;
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;
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;
end;
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 ) }
proof
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;
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; :: thesis: verum