set IR = the InternalRel of R;
set CR = the carrier of R;
per cases ( the carrier of R = {} or not the carrier of R is empty ) ;
suppose A1: the carrier of R = {} ; :: thesis: ex b1 being Relation of (Class (EqRel R)) st
for A, B being object holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
reconsider IT = {} as Relation of (Class (EqRel R)) by RELSET_1:12;
take IT ; :: thesis: for A, B being object holds
( [A,B] in IT iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
let A, B be object ; :: thesis: ( [A,B] in IT iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
thus ( [A,B] in IT implies ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ; :: thesis: ( ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) implies [A,B] in IT )
given a, b being Element of R such that A = Class ((EqRel R),a) and
B = Class ((EqRel R),b) and
A2: a <= b ; :: thesis: [A,B] in IT
the InternalRel of R = {} by A1;
hence [A,B] in IT by A2; :: thesis: verum
end;
suppose not the carrier of R is empty ; :: thesis: ex b1 being Relation of (Class (EqRel R)) st
for A, B being object holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
then reconsider R9 = R as non empty RelStr ;
set IT = { [(Class ((EqRel R),a)),(Class ((EqRel R),b))] where a, b is Element of R9 : a <= b } ;
set Y = Class (EqRel R);
{ [(Class ((EqRel R),a)),(Class ((EqRel R),b))] where a, b is Element of R9 : a <= b } c= [:(Class (EqRel R)),(Class (EqRel R)):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [(Class ((EqRel R),a)),(Class ((EqRel R),b))] where a, b is Element of R9 : a <= b } or x in [:(Class (EqRel R)),(Class (EqRel R)):] )
assume x in { [(Class ((EqRel R),a)),(Class ((EqRel R),b))] where a, b is Element of R9 : a <= b } ; :: thesis: x in [:(Class (EqRel R)),(Class (EqRel R)):]
then consider a, b being Element of R9 such that
A3: x = [(Class ((EqRel R),a)),(Class ((EqRel R),b))] and
a <= b ;
A4: Class ((EqRel R),a) in Class (EqRel R) by EQREL_1:def 3;
Class ((EqRel R),b) in Class (EqRel R) by EQREL_1:def 3;
hence x in [:(Class (EqRel R)),(Class (EqRel R)):] by A3, A4, ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider IT = { [(Class ((EqRel R),a)),(Class ((EqRel R),b))] where a, b is Element of R9 : a <= b } as Relation of (Class (EqRel R)) ;
take IT ; :: thesis: for A, B being object holds
( [A,B] in IT iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
let A, B be object ; :: thesis: ( [A,B] in IT iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
hereby :: thesis: ( ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) implies [A,B] in IT )
assume [A,B] in IT ; :: thesis: ex a9, b9 being Element of R st
( A = Class ((EqRel R),a9) & B = Class ((EqRel R),b9) & a9 <= b9 )
then consider a, b being Element of R such that
A5: [A,B] = [(Class ((EqRel R),a)),(Class ((EqRel R),b))] and
A6: a <= b ;
reconsider a9 = a, b9 = b as Element of R ;
take a9 = a9; :: thesis: ex b9 being Element of R st
( A = Class ((EqRel R),a9) & B = Class ((EqRel R),b9) & a9 <= b9 )
take b9 = b9; :: thesis: ( A = Class ((EqRel R),a9) & B = Class ((EqRel R),b9) & a9 <= b9 )
thus ( A = Class ((EqRel R),a9) & B = Class ((EqRel R),b9) & a9 <= b9 ) by A5, A6, XTUPLE_0:1; :: thesis: verum
end;
given a, b being Element of R such that A7: A = Class ((EqRel R),a) and
A8: B = Class ((EqRel R),b) and
A9: a <= b ; :: thesis: [A,B] in IT
thus [A,B] in IT by A7, A8, A9; :: thesis: verum
end;
end;