let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds
( PA '<' PB iff ERl PA c= ERl PB )
let PA, PB be a_partition of Y; :: thesis: ( PA '<' PB iff ERl PA c= ERl PB )
set RA = ERl PA;
set RB = ERl PB;
hereby :: thesis: ( ERl PA c= ERl PB implies PA '<' PB )
assume A1: PA '<' PB ; :: thesis: ERl PA c= ERl PB
for x1, x2 being object st [x1,x2] in ERl PA holds
[x1,x2] in ERl PB
proof
let x1, x2 be object ; :: thesis: ( [x1,x2] in ERl PA implies [x1,x2] in ERl PB )
assume [x1,x2] in ERl PA ; :: thesis: [x1,x2] in ERl PB
then consider A being Subset of Y such that
A2: A in PA and
A3: ( x1 in A & x2 in A ) by Def6;
ex y being set st
( y in PB & A c= y ) by A1, A2, SETFAM_1:def 2;
hence [x1,x2] in ERl PB by A3, Def6; :: thesis: verum
end;
hence ERl PA c= ERl PB ; :: thesis: verum
end;
assume A4: ERl PA c= ERl PB ; :: thesis: PA '<' PB
for x being set st x in PA holds
ex y being set st
( y in PB & x c= y )
proof
let x be set ; :: thesis: ( x in PA implies ex y being set st
( y in PB & x c= y ) )
assume A5: x in PA ; :: thesis: ex y being set st
( y in PB & x c= y )
then A6: x <> {} by EQREL_1:def 4;
set x0 = the Element of x;
set y = { z where z is Element of Y : [ the Element of x,z] in ERl PB } ;
A7: x c= { z where z is Element of Y : [ the Element of x,z] in ERl PB }
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in x or x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } )
assume A8: x1 in x ; :: thesis: x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB }
then [ the Element of x,x1] in ERl PA by A5, Def6;
hence x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } by A4, A5, A8; :: thesis: verum
end;
set x1 = the Element of x;
[ the Element of x, the Element of x] in ERl PA by A5, A6, Def6;
then consider B being Subset of Y such that
A9: B in PB and
A10: the Element of x in B and
the Element of x in B by A4, Def6;
A11: { z where z is Element of Y : [ the Element of x,z] in ERl PB } c= B
proof
let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } or x2 in B )
assume x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } ; :: thesis: x2 in B
then ex z being Element of Y st
( z = x2 & [ the Element of x,z] in ERl PB ) ;
then consider B2 being Subset of Y such that
A12: B2 in PB and
A13: the Element of x in B2 and
A14: x2 in B2 by Def6;
B2 meets B by A10, A13, XBOOLE_0:3;
hence x2 in B by A9, A12, A14, EQREL_1:def 4; :: thesis: verum
end;
B c= { z where z is Element of Y : [ the Element of x,z] in ERl PB }
proof
let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in B or x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } )
assume A15: x2 in B ; :: thesis: x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB }
then [ the Element of x,x2] in ERl PB by A9, A10, Def6;
hence x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } by A15; :: thesis: verum
end;
then { z where z is Element of Y : [ the Element of x,z] in ERl PB } = B by A11, XBOOLE_0:def 10;
hence ex y being set st
( y in PB & x c= y ) by A7, A9; :: thesis: verum
end;
hence PA '<' PB by SETFAM_1:def 2; :: thesis: verum