H1a: {{1},{3},{4}} c= sring4_8

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{1},{3},{4}} or x in sring4_8 )
assume x in {{1},{3},{4}} ; :: thesis: x in sring4_8
then ( x = {1} or x = {3} or x = {4} ) by ENUMSET1:def 1;
hence x in sring4_8 by ENUMSET1:def 6; :: thesis: verum

end;

H2: {{1},{3},{4}} is Subset-Family of {1,3,4}

proof

{{1},{3},{4}} c= bool {1,3,4}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{1},{3},{4}} or x in bool {1,3,4} )
assume x in {{1},{3},{4}} ; :: thesis: x in bool {1,3,4}
then AAA: ( x = {1} or x = {3} or x = {4} ) by ENUMSET1:def 1;
( {1} c= {1,3,4} & {3} c= {1,3,4} & {4} c= {1,3,4} )

proof

thus {1} c= {1,3,4} :: thesis: ( {3} c= {1,3,4} & {4} c= {1,3,4} )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in {1,3,4} )
assume x in {1} ; :: thesis: x in {1,3,4}
then x = 1 by TARSKI:def 1;
hence x in {1,3,4} by ENUMSET1:def 1; :: thesis: verum

end;

thus {3} c= {1,3,4} :: thesis: {4} c= {1,3,4}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {3} or x in {1,3,4} )
assume x in {3} ; :: thesis: x in {1,3,4}
then x = 3 by TARSKI:def 1;
hence x in {1,3,4} by ENUMSET1:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {4} or x in {1,3,4} )
assume x in {4} ; :: thesis: x in {1,3,4}
then x = 4 by TARSKI:def 1;
hence x in {1,3,4} by ENUMSET1:def 1; :: thesis: verum

end;

hence x in bool {1,3,4} by AAA; :: thesis: verum

end;

hence {{1},{3},{4}} is Subset-Family of {1,3,4} ; :: thesis: verum

end;

H3: union {{1},{3},{4}} = {1,3,4}

proof

T1: ( union {{1}} = {1} & union {{3},{4}} = {3,4} ) by ZFMISC_1:26;
T1A: union {{1},{3},{4}} = union ({{1}} \/ {{3},{4}}) by ENUMSET1:2;
{1} \/ {3,4} = {1,3,4} by ENUMSET1:2;
hence union {{1},{3},{4}} = {1,3,4} by T1, T1A, ZFMISC_1:78; :: thesis: verum

end;

for x being Subset of {1,3,4} st x in {{1},{3},{4}} holds
( x <> {} & ( for y being Subset of {1,3,4} holds
( not y in {{1},{3},{4}} or x = y or x misses y ) ) )

proof

let x be Subset of {1,3,4}; :: thesis: ( x in {{1},{3},{4}} implies ( x <> {} & ( for y being Subset of {1,3,4} holds
( not y in {{1},{3},{4}} or x = y or x misses y ) ) ) )
assume AA0: x in {{1},{3},{4}} ; :: thesis: ( x <> {} & ( for y being Subset of {1,3,4} holds
( not y in {{1},{3},{4}} or x = y or x misses y ) ) )
hence x <> {} ; :: thesis: for y being Subset of {1,3,4} holds
( not y in {{1},{3},{4}} or x = y or x misses y )
for y being Subset of {1,3,4} holds
( not y in {{1},{3},{4}} or x = y or x misses y )

proof

let y be Subset of {1,3,4}; :: thesis: ( not y in {{1},{3},{4}} or x = y or x misses y )
assume y in {{1},{3},{4}} ; :: thesis: ( x = y or x misses y )
then ( ( y = {1} or y = {3} or y = {4} ) & ( x = {1} or x = {3} or x = {4} ) ) by AA0, ENUMSET1:def 1;
hence ( x = y or x misses y ) by LL18, LL19, LL24; :: thesis: verum

end;

hence for y being Subset of {1,3,4} holds
( not y in {{1},{3},{4}} or x = y or x misses y ) ; :: thesis: verum

end;

hence ( {{1},{3},{4}} is Subset of sring4_8 & {{1},{3},{4}} is a_partition of {1,3,4} ) by H1a, H2, H3, EQREL_1:def 4; :: thesis: verum