let x1, x2 be object ; :: thesis: for Z being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
let Z be set ; :: thesis: ( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
thus ( not Z c= {x1,x2} or Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) :: thesis: ( ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) implies Z c= {x1,x2} )
proof
assume that
A1: Z c= {x1,x2} and
A2: Z <> {} and
A3: Z <> {x1} and
A4: Z <> {x2} ; :: thesis: Z = {x1,x2}
now :: thesis: for z being object holds
( ( z in Z implies z in {x1,x2} ) & ( z in {x1,x2} implies z in Z ) )
let z be object ; :: thesis: ( ( z in Z implies z in {x1,x2} ) & ( z in {x1,x2} implies z in Z ) )
thus ( z in Z implies z in {x1,x2} ) by A1; :: thesis: ( z in {x1,x2} implies z in Z )
A5: now :: thesis: x1 in Z
assume A6: not x1 in Z ; :: thesis: contradiction
consider y being object such that
A7: y in Z and
A8: y <> x2 by A2, A4, Lm12;
y in {x1,x2} by A1, A7;
hence contradiction by A6, A7, A8, TARSKI:def 2; :: thesis: verum
end;
A9: now :: thesis: x2 in Z
assume A10: not x2 in Z ; :: thesis: contradiction
consider y being object such that
A11: y in Z and
A12: y <> x1 by A2, A3, Lm12;
y in {x1,x2} by A1, A11;
hence contradiction by A10, A11, A12, TARSKI:def 2; :: thesis: verum
end;
assume z in {x1,x2} ; :: thesis: z in Z
hence z in Z by A5, A9, TARSKI:def 2; :: thesis: verum
end;
hence Z = {x1,x2} by TARSKI:2; :: thesis: verum
end;
thus ( ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) implies Z c= {x1,x2} ) by Th7; :: thesis: verum