let Y be non empty set ; :: thesis: for a being Element of Funcs 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 Element of Funcs 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 )
assume A1: a is_dependent_of PA ; :: thesis: 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 = { x' where x' is Element of Y : S₂[x'] } as Subset of Y from DOMAIN_1:sch 7();
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 ) )
assume A2: g in PA ; :: thesis: ex h being set st
( h in GPart a & g c= h )
then A3: ( g c= Y & g <> {} ) by EQREL_1:def 6;
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;

consider u being Element of g;
u in g by A3;
then reconsider u = u as Element of Y by A2;

now

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 )

then u in C ;
then A6: not C in {{} } by TARSKI:def 1;
C in {C,D} by TARSKI:def 2;
then A7: C in {C,D} \ {{} } by A6, XBOOLE_0:def 5;
g c= C

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in g or t in C )
assume A8: t in g ; :: thesis: t in C
then reconsider t = t as Element of Y by A2;

now

per cases ( a . t = TRUE or a . t = FALSE ) by A4, A8;

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, A8, Def18; :: thesis: verum

end;

end;

end;

hence t in C ; :: thesis: verum

end;

hence ex h being set st
( h in GPart a & g c= h ) by A7; :: thesis: verum

end;

case A9: a . u = FALSE ; :: thesis: ex h being set st
( h in GPart a & g c= h )

then u in D ;
then A10: not D in {{} } by TARSKI:def 1;
D in {C,D} by TARSKI:def 2;
then A11: D in {C,D} \ {{} } by A10, XBOOLE_0:def 5;
g c= D

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in g or t in D )
assume A12: t in g ; :: thesis: t in D
then reconsider t = t as Element of Y by A2;

now

per cases ( a . t = TRUE or a . t = FALSE ) by A4, A12;

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

hence contradiction by A1, A2, A9, A12, Def18; :: 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;

hence ex h being set st
( h in GPart a & g c= h ) by A11; :: 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