sring4_8 is cap-finite-partition-closed

proof

let S1, S2 be Element of sring4_8 ; :: according to SRINGS_1:def 1 :: thesis: ( S1 /\ S2 is empty or ex b₁ being Element of bool sring4_8 st b₁ is a_partition of S1 /\ S2 )
assume not S1 /\ S2 is empty ; :: thesis: ex b₁ being Element of bool sring4_8 st b₁ is a_partition of S1 /\ S2
S1 /\ S2 in INTERSECTION (sring4_8,sring4_8) by SETFAM_1:def 5;
then consider P being finite Subset of sring4_8 such that
A5: P is a_partition of S1 /\ S2 by LemC;
take P ; :: thesis: P is a_partition of S1 /\ S2
thus P is a_partition of S1 /\ S2 by A5; :: thesis: verum

end;

hence sring4_8 is cap-finite-partition-closed ; :: thesis: not sring4_8 is cap-closed
assume H2: sring4_8 is cap-closed ; :: thesis: contradiction
( {1,2,3} in sring4_8 & {2,3,4} in sring4_8 ) by ENUMSET1:def 6;
hence contradiction by LemA, H2, FINSUB_1:def 2; :: thesis: verum