let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a
let a be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a
let PA be a_partition of Y; :: thesis: ( a is_dependent_of PA implies PA is_finer_than GPart a )
defpred S1[ set ] means a . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S1[x] } as Subset of Y from DOMAIN_1:sch 7();
 defpred S2[ set ] means a . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S2[x9] } as Subset of Y from DOMAIN_1:sch 7();
 assume A1: a is_dependent_of PA ; :: thesis: PA is_finer_than GPart a
for g being set st g in PA holds
ex h being set st
( h in GPart a & g c= h )
proof
let g be set ; :: thesis: ( g in PA implies ex h being set st
( h in GPart a & g c= h ) )
set u = the Element of g;
assume A2: g in PA ; :: thesis: ex h being set st
( h in GPart a & g c= h )
then A3: g <> {} by EQREL_1:def 4;
then the Element of g in g ;
then reconsider u = the Element of g as Element of Y by A2;
A4: for x1 being set holds
( not x1 in g or a . x1 = TRUE or a . x1 = FALSE )
proof
let x1 be set ; :: thesis: ( not x1 in g or a . x1 = TRUE or a . x1 = FALSE )
assume x1 in g ; :: thesis: ( a . x1 = TRUE or a . x1 = FALSE )
then reconsider x1 = x1 as Element of Y by A2;
a . x1 in BOOLEAN ;
hence ( a . x1 = TRUE or a . x1 = FALSE ) by TARSKI:def 2; :: thesis: verum
end;
now :: thesis: ( ( a . u = TRUE & ex h being set st
( h in GPart a & g c= h ) ) or ( a . u = FALSE & ex h being set st
( h in GPart a & g c= h ) ) )
per cases ( a . u = TRUE or a . u = FALSE ) by A3, A4;
case A5: a . u = TRUE ; :: thesis: ex h being set st
( h in GPart a & g c= h )
A6: g c= C
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in g or t in C )
assume A7: t in g ; :: thesis: t in C
then reconsider t = t as Element of Y by A2;
now :: thesis: ( ( a . t = TRUE & t in C ) or ( a . t = FALSE & contradiction ) )
per cases ( a . t = TRUE or a . t = FALSE ) by A4, A7;
case a . t = TRUE ; :: thesis: t in C
hence t in C ; :: thesis: verum
end;
end;
end;
hence t in C ; :: thesis: verum
end;
u in C by A5;
then A8: not C in {{}} by TARSKI:def 1;
C in {C,D} by TARSKI:def 2;
then C in {C,D} \ {{}} by A8, XBOOLE_0:def 5;
hence ex h being set st
( h in GPart a & g c= h ) by A6; :: thesis: verum
end;
case A9: a . u = FALSE ; :: thesis: ex h being set st
( h in GPart a & g c= h )
A10: g c= D
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in g or t in D )
assume A11: t in g ; :: thesis: t in D
then reconsider t = t as Element of Y by A2;
now :: thesis: ( ( a . t = TRUE & contradiction ) or ( a . t = FALSE & t in D ) )
per cases ( a . t = TRUE or a . t = FALSE ) by A4, A11;
end;
end;
hence t in D ; :: thesis: verum
end;
u in D by A9;
then A12: not D in {{}} by TARSKI:def 1;
D in {C,D} by TARSKI:def 2;
then D in {C,D} \ {{}} by A12, XBOOLE_0:def 5;
hence ex h being set st
( h in GPart a & g c= h ) by A10; :: thesis: verum
end;
end;
end;
hence ex h being set st
( h in GPart a & g c= h ) ; :: thesis: verum
end;
hence PA is_finer_than GPart a by SETFAM_1:def 2; :: thesis: verum