H1a: {{2},{3}} c= sring4_8

proof

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

end;

H2: {{2},{3}} is Subset-Family of {2,3}

proof

{{2},{3}} c= bool {2,3}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{2},{3}} or x in bool {2,3} )
assume x in {{2},{3}} ; :: thesis: x in bool {2,3}
then AAA: ( x = {2} or x = {3} ) by TARSKI:def 2;
( {2} c= {2,3} & {3} c= {2,3} ) by ZFMISC_1:7;
hence x in bool {2,3} by AAA; :: thesis: verum

end;

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

end;

H3: union {{2},{3}} = {2,3} by ZFMISC_1:26;
for x being Subset of {2,3} st x in {{2},{3}} holds
( x <> {} & ( for y being Subset of {2,3} holds
( not y in {{2},{3}} or x = y or x misses y ) ) )

proof

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

proof

let y be Subset of {2,3}; :: thesis: ( not y in {{2},{3}} or x = y or x misses y )
assume y in {{2},{3}} ; :: thesis: ( x = y or x misses y )
then ( ( y = {2} or y = {3} ) & ( x = {2} or x = {3} ) ) by AA0, TARSKI:def 2;
hence ( x = y or x misses y ) by LL21; :: thesis: verum

end;

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

end;

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