set M2 = multiples 2;
set M3 = multiples 3;
set M23 = (multiples 2) \/ (multiples 3);
set M5 = multiples 5;
set M = ((multiples 2) \/ (multiples 3)) \/ (multiples 5);
set S = seq (0,30);
((multiples 2) \/ (multiples 3)) \/ (multiples 5) = ((multiples 2) \/ (multiples 3)) \/ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) by XBOOLE_1:39;
then A1: (seq (0,30)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) = ((seq (0,30)) /\ ((multiples 2) \/ (multiples 3))) \/ ((seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3)))) by XBOOLE_1:23;
A2: card ((seq (0,30)) /\ ((multiples 2) \/ (multiples 3))) = 20

proof

6 = 2 * 3 ;
then A3: ( 2 divides 6 & 3 divides 6 ) ;
(multiples 2) \/ (multiples 3) = ((multiples 2) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6
.= (((multiples 2) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6
.= ((((multiples 2) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6 ;
then card ((seq (0,(5 * 6))) /\ ((multiples 2) \/ (multiples 3))) = 5 * (card ((seq ((0 * 6),6)) /\ ((multiples 2) \/ (multiples 3)))) by A3, Th90
.= 5 * 4 by Th91 ;
hence card ((seq (0,30)) /\ ((multiples 2) \/ (multiples 3))) = 20 ; :: thesis: verum

end;

A4: (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) = {5,25}

proof

( (2 * 2) + 1 = 5 & (12 * 2) + 1 = 25 ) ;
then ( not 2 divides 5 & not 2 divides 25 ) ;
then A5: ( not 5 in multiples 2 & not 25 in multiples 2 ) by NUMBER14:62;
( (3 * 1) + 2 = 5 & (8 * 3) + 1 = 25 ) ;
then ( not 5 in multiples 3 & not 25 in multiples 3 ) by NAT_4:9, NUMBER14:62;
then A6: ( not 5 in (multiples 2) \/ (multiples 3) & not 25 in (multiples 2) \/ (multiples 3) ) by A5, XBOOLE_0:def 3;
( 5 * 1 = 5 & 5 * 5 = 25 ) ;
then ( 5 divides 5 & 5 divides 25 ) ;
then ( 5 in multiples 5 & 25 in multiples 5 ) by NUMBER14:62;
then A7: ( 5 in (multiples 5) \ ((multiples 2) \/ (multiples 3)) & 25 in (multiples 5) \ ((multiples 2) \/ (multiples 3)) ) by A6, XBOOLE_0:def 5;
( 0 < 5 & 5 <= 0 + 30 & 0 < 25 & 25 <= 0 + 30 ) ;
then ( 5 in seq (0,30) & 25 in seq (0,30) ) by Th73;
then ( 5 in (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) & 25 in (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) ) by A7, XBOOLE_0:def 4;
then A8: {5,25} c= (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) by ZFMISC_1:32;
(seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) c= {5,25}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) or y in {5,25} )
assume A9: y in (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) ; :: thesis: y in {5,25}
then reconsider y = y as Nat ;
A10: ( y in multiples 5 & not y in (multiples 2) \/ (multiples 3) ) by A9, XBOOLE_0:def 5;
then consider k being Nat such that
A11: y = 5 * k by NAT_D:def 3, NUMBER14:62;
( not y in multiples 2 & not y in multiples 3 ) by A10, XBOOLE_0:def 3;
then A12: ( not 2 divides y & not 3 divides y ) by NUMBER14:62;
( 0 * 5 = 0 & 0 < 5 * k & 5 * k <= 0 + 30 & 0 + 30 = 5 * 6 ) by A9, A11, Th73;
then ( 0 < k & k <= 6 ) by XREAL_1:68;
then not not k = 0 & ... & not k = 6 ;

per cases then ( k = 2 or k = 4 or k = 6 or k = 3 or k = 1 or k = 5 ) by A9, A11, Th73;

suppose ( k = 2 or k = 4 or k = 6 ) ; :: thesis: y in {5,25}

then ( y = 2 * 5 or y = 2 * (5 * 2) or y = 2 * (5 * 3) ) by A11;
hence y in {5,25} by A12; :: thesis: verum

end;

suppose k = 3 ; :: thesis: y in {5,25}

hence y in {5,25} by A11, A12; :: thesis: verum

end;

suppose ( k = 1 or k = 5 ) ; :: thesis: y in {5,25}

hence y in {5,25} by A11, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence (seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) = {5,25} by A8, XBOOLE_0:def 10; :: thesis: verum

end;

A13: card ((seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3)))) = 2 by A4, CARD_2:57;
(multiples 2) \/ (multiples 3) misses (multiples 5) \ ((multiples 2) \/ (multiples 3)) by XBOOLE_1:79;
then card ((seq (0,30)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = (card ((seq (0,30)) /\ ((multiples 2) \/ (multiples 3)))) + (card ((seq (0,30)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))))) by A1, XBOOLE_1:76, CARD_2:40;
hence 22 = card ((seq (0,30)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) by A2, A13; :: thesis: verum