set SF = {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} c= bool {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in bool {1,2,3,4} )
assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} ; :: thesis: x in bool {1,2,3,4}
then S1: ( x = {1,2,3,4} or x = {1,2,3} or x = {2,3,4} or x = {1} or x = {2} or x = {3} or x = {4} or x = {} ) by ENUMSET1:def 6;
reconsider x = x as set by TARSKI:1;
S3: {1,2,3} c= {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1,2,3} or x in {1,2,3,4} )
assume x in {1,2,3} ; :: thesis: x in {1,2,3,4}
then ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum
end;
S4: {2,3,4} c= {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {2,3,4} or x in {1,2,3,4} )
assume x in {2,3,4} ; :: thesis: x in {1,2,3,4}
then ( x = 2 or x = 3 or x = 4 ) by ENUMSET1:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum
end;
S5: {1} c= {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in {1,2,3,4} )
assume x in {1} ; :: thesis: x in {1,2,3,4}
then x = 1 by TARSKI:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum
end;
S6: {2} c= {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {2} or x in {1,2,3,4} )
assume x in {2} ; :: thesis: x in {1,2,3,4}
then x = 2 by TARSKI:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum
end;
S7: {3} c= {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {3} or x in {1,2,3,4} )
assume x in {3} ; :: thesis: x in {1,2,3,4}
then x = 3 by TARSKI:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum
end;
S8: {4} c= {1,2,3,4}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {4} or x in {1,2,3,4} )
assume x in {4} ; :: thesis: x in {1,2,3,4}
then x = 4 by TARSKI:def 1;
hence x in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum
end;
x c= {1,2,3,4} by S1, S3, S4, S5, S6, S7, S8;
hence x in bool {1,2,3,4} ; :: thesis: verum
end;
hence {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} is Subset-Family of {1,2,3,4} ; :: thesis: verum