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 S₁[ set ] means a . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S₁[x] } as Subset of Y from DOMAIN_1:sch 7();
defpred S₂[ set ] means a . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S₂[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;

case a . t = FALSE ; :: thesis: contradiction

hence contradiction by A1, A2, A5, A7; :: 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;

case a . t = TRUE ; :: thesis: contradiction

hence contradiction by A1, A2, A9, A11; :: thesis: verum

end;

case a . t = FALSE ; :: thesis: t in D

hence t in D ; :: thesis: verum

end;

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